Theorem ifnefalse 3941

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 3938 directly in this case. It happens, e.g., in oevn0 7157. (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 2651	. 2 |- ( A =/= B <-> -. A = B )
2		iffalse 3938	. 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 1398   =/= wne 2649   ifcif 3929

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-ne 2651  df-if 3930

This theorem is referenced by:  xpima2  5436  axcc2lem  8807  xnegmnf  11412  rexneg  11413  xaddpnf1  11428  xaddpnf2  11429  xaddmnf1  11430  xaddmnf2  11431  mnfaddpnf  11433  rexadd  11434  fztpval  11745  sadcp1  14189  smupp1  14214  pcval  14452  ramtcl  14612  ramub1lem1  14628  xpscfv  15051  xpsfrnel  15052  gexlem2  16801  frgpuptinv  16988  frgpup3lem  16994  gsummpt1n0  17188  dprdfid  17252  dprdfidOLD  17259  dpjrid  17306  abvtrivd  17684  mplsubrg  18297  znf1o  18763  znhash  18770  znunithash  18776  mamulid  19110  mamurid  19111  dmatid  19164  dmatmulcl  19169  scmatdmat  19184  mdetdiagid  19269  chpdmatlem2  19507  chpscmat  19510  chpidmat  19515  xkoccn  20286  iccpnfhmeo  21611  xrhmeo  21612  ioorinv2  22150  mbfi1fseqlem4  22291  ellimc2  22447  dvcobr  22515  ply1remlem  22729  dvtaylp  22931  0cxp  23215  lgsval3  23787  lgsdinn0  23813  dchrisumlem1  23872  dchrvmasumiflem1  23884  rpvmasum2  23895  dchrvmasumlem  23906  padicabv  24013  indispcon  28943  fnejoin1  30426  fdc  30478  sdrgacs  31391  blenn0  33448  cdlemk40f  37042