Theorem ifnefalse 3951

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 3948 directly in this case. It happens, e.g., in oevn0 7166. (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 2664	. 2 |- ( A =/= B <-> -. A = B )
2		iffalse 3948	. 2 |- ( -. A = B -> if ( A = B , C , D ) = D )
3	1, 2	sylbi 195	1 |- ( A =/= B -> if ( A = B , C , D ) = D )

Syntax hints:   -. wn 3   -> wi 4   = wceq 1379   =/= wne 2662   ifcif 3939

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-ne 2664  df-if 3940

This theorem is referenced by:  xpima2  5451  axcc2lem  8817  xnegmnf  11410  rexneg  11411  xaddpnf1  11426  xaddpnf2  11427  xaddmnf1  11428  xaddmnf2  11429  mnfaddpnf  11431  rexadd  11432  fztpval  11742  sadcp1  13967  smupp1  13992  pcval  14230  ramtcl  14390  ramub1lem1  14406  xpscfv  14820  xpsfrnel  14821  gexlem2  16417  frgpuptinv  16604  frgpup3lem  16610  gsummpt1n0  16807  dprdfid  16871  dprdfidOLD  16878  dpjrid  16925  abvtrivd  17301  mplsubrg  17913  znf1o  18397  znhash  18404  znunithash  18410  mamulid  18750  mamurid  18751  dmatid  18804  dmatmulcl  18809  scmatdmat  18824  mdetdiagid  18909  chpdmatlem2  19147  chpscmat  19150  chpidmat  19155  xkoccn  19947  iccpnfhmeo  21272  xrhmeo  21273  ioorinv2  21811  mbfi1fseqlem4  21952  ellimc2  22108  dvcobr  22176  ply1remlem  22390  dvtaylp  22591  0cxp  22872  lgsval3  23414  lgsdinn0  23440  dchrisumlem1  23499  dchrvmasumiflem1  23511  rpvmasum2  23522  dchrvmasumlem  23533  padicabv  23640  indispcon  28430  fnejoin1  30016  fdc  30068  sdrgacs  30982  cdlemk40f  35932