Theorem ifnefalse 4497

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

Assertion

Ref	Expression
ifnefalse	⊢ (𝐴 ≠ 𝐵 → if(𝐴 = 𝐵, 𝐶, 𝐷) = 𝐷)

Proof of Theorem ifnefalse

Step	Hyp	Ref	Expression
1		df-ne 2958	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2		iffalse 4494	. 2 ⊢ (¬ 𝐴 = 𝐵 → if(𝐴 = 𝐵, 𝐶, 𝐷) = 𝐷)
3	1, 2	sylbi 220	1 ⊢ (𝐴 ≠ 𝐵 → if(𝐴 = 𝐵, 𝐶, 𝐷) = 𝐷)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1570   ≠ wne 2957  ifcif 4485

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-if 4486

This theorem is used by:  xpima2  6181  axcc2lem  10441  xnegmnf  13264  rexneg  13265  xaddpnf1  13280  xaddpnf2  13281  xaddmnf1  13282  xaddmnf2  13283  mnfaddpnf  13285  rexadd  13286  fztpval  13643  sadcp1  16549  smupp1  16574  pcval  16940  ramtcl  17106  ramub1lem1  17122  xpsfrnel  17652  gexlem2  19710  frgpuptinv  19899  frgpup3lem  19905  gsummpt1n0  20093  dprdfid  20147  dpjrid  20192  sdrgacs  20968  abvtrivd  20999  znf1o  21765  znhash  21772  znunithash  21778  mplsubrg  22220  psdmul  22395  mamulid  22664  mamurid  22665  dmatid  22718  dmatmulcl  22723  scmatdmat  22738  mdetdiagid  22823  chpdmatlem2  23065  chpscmat  23068  chpidmat  23073  xkoccn  23846  iccpnfhmeo  25174  xrhmeo  25175  ioorinv2  25804  mbfi1fseqlem4  25947  ellimc2  26106  dvcobr  26175  ply1remlem  26392  dvtaylp  26603  0cxp  26901  lgsval3  27549  lgsdinn0  27579  dchrisumlem1  27723  dchrvmasumiflem1  27735  rpvmasum2  27746  dchrvmasumlem  27757  padicabv  27864  indispconn  35800  ex-sategoelel  35987  fnejoin1  36974  ptrecube  38356  poimirlem16  38372  poimirlem17  38373  poimirlem19  38375  poimirlem20  38376  fdc  38482  cdlemk40f  41779  fiabv  43405  blenn0  49490