Theorem ifnefalse 3938

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 3935 directly in this case. It happens, e.g., in oevn0 7167. (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 2640	. 2 |- ( A =/= B <-> -. A = B )
2		iffalse 3935	. 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 1383   =/= wne 2638   ifcif 3926

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-ne 2640  df-if 3927

This theorem is referenced by:  xpima2  5441  axcc2lem  8819  xnegmnf  11418  rexneg  11419  xaddpnf1  11434  xaddpnf2  11435  xaddmnf1  11436  xaddmnf2  11437  mnfaddpnf  11439  rexadd  11440  fztpval  11750  sadcp1  13982  smupp1  14007  pcval  14245  ramtcl  14405  ramub1lem1  14421  xpscfv  14836  xpsfrnel  14837  gexlem2  16476  frgpuptinv  16663  frgpup3lem  16669  gsummpt1n0  16866  dprdfid  16931  dprdfidOLD  16938  dpjrid  16985  abvtrivd  17363  mplsubrg  17976  znf1o  18463  znhash  18470  znunithash  18476  mamulid  18816  mamurid  18817  dmatid  18870  dmatmulcl  18875  scmatdmat  18890  mdetdiagid  18975  chpdmatlem2  19213  chpscmat  19216  chpidmat  19221  xkoccn  19993  iccpnfhmeo  21318  xrhmeo  21319  ioorinv2  21857  mbfi1fseqlem4  21998  ellimc2  22154  dvcobr  22222  ply1remlem  22436  dvtaylp  22637  0cxp  22919  lgsval3  23461  lgsdinn0  23487  dchrisumlem1  23546  dchrvmasumiflem1  23558  rpvmasum2  23569  dchrvmasumlem  23580  padicabv  23687  indispcon  28552  fnejoin1  30161  fdc  30213  sdrgacs  31126  cdlemk40f  36385