Theorem ifnefalse 3953

Description: When values are unequal, but an "if" condition checks if they are equal, then the "false" branch results. This is a simple utility to provide a slight shortening and simplification of proofs vs. applying iffalse 3950 directly in this case. It happens, e.g., in oevn0 7184. (Contributed by David A. Wheeler, 15-May-2015.)

Assertion

Ref	Expression
ifnefalse

Proof of Theorem ifnefalse

Step	Hyp	Ref	Expression
1		df-ne 2654	. 2
2		iffalse 3950	. 2
3	1, 2	sylbi 195	1

Syntax hints:  -.wn 3  ->wi 4  =wceq 1395  =/=wne 2652  ifcif 3941

This theorem is referenced by:  xpima2  5456  axcc2lem  8837  xnegmnf  11438  rexneg  11439  xaddpnf1  11454  xaddpnf2  11455  xaddmnf1  11456  xaddmnf2  11457  mnfaddpnf  11459  rexadd  11460  fztpval  11770  sadcp1  14105  smupp1  14130  pcval  14368  ramtcl  14528  ramub1lem1  14544  xpscfv  14959  xpsfrnel  14960  gexlem2  16602  frgpuptinv  16789  frgpup3lem  16795  gsummpt1n0  16992  dprdfid  17057  dprdfidOLD  17064  dpjrid  17111  abvtrivd  17489  mplsubrg  18102  znf1o  18590  znhash  18597  znunithash  18603  mamulid  18943  mamurid  18944  dmatid  18997  dmatmulcl  19002  scmatdmat  19017  mdetdiagid  19102  chpdmatlem2  19340  chpscmat  19343  chpidmat  19348  xkoccn  20120  iccpnfhmeo  21445  xrhmeo  21446  ioorinv2  21984  mbfi1fseqlem4  22125  ellimc2  22281  dvcobr  22349  ply1remlem  22563  dvtaylp  22765  0cxp  23047  lgsval3  23589  lgsdinn0  23615  dchrisumlem1  23674  dchrvmasumiflem1  23686  rpvmasum2  23697  dchrvmasumlem  23708  padicabv  23815  indispcon  28679  fnejoin1  30186  fdc  30238  sdrgacs  31150  cdlemk40f  36645

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-ne 2654  df-if 3942