Theorem eqneqall 2805

Description: A contradiction concerning equality implies anything. (Contributed by Alexander van der Vekens, 25-Jan-2018.)

Assertion

Ref	Expression
eqneqall	|- ( A = B -> ( A =/= B -> ph ) )

Proof of Theorem eqneqall

Step	Hyp	Ref	Expression
1		df-ne 2795	. 2 |- ( A =/= B <-> -. A = B )
2		pm2.24 121	. 2 |- ( A = B -> ( -. A = B -> ph ) )
3	1, 2	syl5bi 232	1 |- ( A = B -> ( A =/= B -> ph ) )

Syntax hints:   -. wn 3   -> wi 4   = wceq 1483   =/= wne 2794

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-ne 2795

This theorem is referenced by:  nonconne  2806  ssprsseq  4357  prnebg  4389  3elpr2eq  4435  propssopi  4971  iunopeqop  4981  tpres  6466  elovmpt3imp  6890  bropopvvv  7255  bropfvvvvlem  7256  fin1a2lem10  9231  modfzo0difsn  12742  suppssfz  12794  hashrabsn1  13163  hash2pwpr  13258  hashle2pr  13259  hashge2el2difr  13263  cshwidxmod  13549  cshwidx0  13552  mod2eq1n2dvds  15071  nno  15098  prm2orodd  15404  prm23lt5  15519  dvdsprmpweqnn  15589  symgextf1  17841  01eq0ring  19272  mamufacex  20195  mavmulsolcl  20357  chfacfscmulgsum  20665  chfacfpmmulgsum  20669  lgsqrmodndvds  25078  gausslemma2dlem0f  25086  gausslemma2dlem0i  25089  2lgs  25132  2lgsoddprm  25141  umgrnloop2  26041  uhgr2edg  26100  uvtxa01vtx0  26297  g0wlk0  26548  wlkreslem  26566  upgrwlkdvdelem  26632  uspgrn2crct  26700  wspn0  26820  2pthdlem1  26826  2pthon3v  26839  umgr2adedgspth  26844  umgrclwwlksge2  26912  lppthon  27011  1pthon2v  27013  frgrwopreglem4a  27174  frgrreg  27252  frgrregord13  27254  frgrogt3nreg  27255  nsnlplig  27333  nsnlpligALT  27334  goldbachth  41459  lighneallem2  41523  lighneal  41528  evenltle  41626  lidldomn1  41921  nzerooringczr  42072  ztprmneprm  42125  suppmptcfin  42160  linc1  42214  lindsrng01  42257  ldepspr  42262  zlmodzxznm  42286