Theorem ifnefalse 3893

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 3890 directly in this case. It happens, e.g., in oevn0 7217. (Contributed by David A. Wheeler, 15-May-2015.)

Assertion

Ref	Expression
ifnefalse	|- ( A =/= B -> if ( A = B , C , D ) = D )

Proof of Theorem ifnefalse

Step	Hyp	Ref	Expression
1		df-ne 2624	. 2 |- ( A =/= B <-> -. A = B )
2		iffalse 3890	. 2 |- ( -. A = B -> if ( A = B , C , D ) = D )
3	1, 2	sylbi 199	1 |- ( A =/= B -> if ( A = B , C , D ) = D )

Syntax hints:   -. wn 3   -> wi 4   = wceq 1444   =/= wne 2622   ifcif 3881

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-ne 2624  df-if 3882

This theorem is referenced by:  xpima2  5281  axcc2lem  8866  xnegmnf  11503  rexneg  11504  xaddpnf1  11519  xaddpnf2  11520  xaddmnf1  11521  xaddmnf2  11522  mnfaddpnf  11524  rexadd  11525  fztpval  11857  sadcp1  14429  smupp1  14454  pcval  14794  ramtcl  14964  ramtclOLD  14965  ramub1lem1  14984  xpscfv  15468  xpsfrnel  15469  gexlem2  17233  gexlem2OLD  17236  frgpuptinv  17421  frgpup3lem  17427  gsummpt1n0  17597  dprdfid  17650  dpjrid  17695  abvtrivd  18068  mplsubrg  18664  znf1o  19122  znhash  19129  znunithash  19135  mamulid  19466  mamurid  19467  dmatid  19520  dmatmulcl  19525  scmatdmat  19540  mdetdiagid  19625  chpdmatlem2  19863  chpscmat  19866  chpidmat  19871  xkoccn  20634  iccpnfhmeo  21973  xrhmeo  21974  ioorinv2  22527  ioorinv2OLD  22532  mbfi1fseqlem4  22676  ellimc2  22832  dvcobr  22900  ply1remlem  23113  dvtaylp  23325  0cxp  23611  lgsval3  24242  lgsdinn0  24268  dchrisumlem1  24327  dchrvmasumiflem1  24339  rpvmasum2  24350  dchrvmasumlem  24361  padicabv  24468  indispcon  29957  fnejoin1  31024  ptrecube  31940  poimirlem16  31956  poimirlem17  31957  poimirlem19  31959  poimirlem20  31960  fdc  32074  cdlemk40f  34486  sdrgacs  36067  blenn0  40437