Theorem ifnefalse 3813

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 3811 directly in this case. It happens, e.g., in oevn0 6967. (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 2620	. 2 |- ( A =/= B <-> -. A = B )
2		iffalse 3811	. 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 1369   =/= wne 2618   ifcif 3803

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-ne 2620  df-if 3804

This theorem is referenced by:  xpima2  5294  axcc2lem  8617  xnegmnf  11192  rexneg  11193  xaddpnf1  11208  xaddpnf2  11209  xaddmnf1  11210  xaddmnf2  11211  mnfaddpnf  11213  rexadd  11214  fztpval  11530  sadcp1  13663  smupp1  13688  pcval  13923  ramtcl  14083  ramub1lem1  14099  xpscfv  14512  xpsfrnel  14513  gexlem2  16093  frgpuptinv  16280  frgpup3lem  16286  gsummpt1n0  16468  dprdfid  16519  dprdfidOLD  16526  dpjrid  16573  abvtrivd  16937  mplsubrg  17531  znf1o  17996  znhash  18003  znunithash  18009  mamulid  18316  mamurid  18317  xkoccn  19204  iccpnfhmeo  20529  xrhmeo  20530  ioorinv2  21067  mbfi1fseqlem4  21208  ellimc2  21364  dvcobr  21432  ply1remlem  21646  dvtaylp  21847  0cxp  22123  lgsval3  22665  lgsdinn0  22691  dchrisumlem1  22750  dchrvmasumiflem1  22762  rpvmasum2  22773  dchrvmasumlem  22784  padicabv  22891  indispcon  27135  fnejoin1  28601  fdc  28653  sdrgacs  29570  dmatid  30886  dmatmulcl  30891  scmatdmat  30895  mdetdiagid  30949  cdlemk40f  34575