Theorem ifnefalse 4098

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

Assertion

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

Proof of Theorem ifnefalse

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1483   ≠ wne 2794  ifcif 4086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-ne 2795  df-if 4087

This theorem is referenced by:  xpima2  5578  axcc2lem  9258  xnegmnf  12041  rexneg  12042  xaddpnf1  12057  xaddpnf2  12058  xaddmnf1  12059  xaddmnf2  12060  mnfaddpnf  12062  rexadd  12063  fztpval  12402  sadcp1  15177  smupp1  15202  pcval  15549  ramtcl  15714  ramub1lem1  15730  xpscfv  16222  xpsfrnel  16223  gexlem2  17997  frgpuptinv  18184  frgpup3lem  18190  gsummpt1n0  18364  dprdfid  18416  dpjrid  18461  abvtrivd  18840  mplsubrg  19440  znf1o  19900  znhash  19907  znunithash  19913  mamulid  20247  mamurid  20248  dmatid  20301  dmatmulcl  20306  scmatdmat  20321  mdetdiagid  20406  chpdmatlem2  20644  chpscmat  20647  chpidmat  20652  xkoccn  21422  iccpnfhmeo  22744  xrhmeo  22745  ioorinv2  23343  mbfi1fseqlem4  23485  ellimc2  23641  dvcobr  23709  ply1remlem  23922  dvtaylp  24124  0cxp  24412  lgsval3  25040  lgsdinn0  25070  dchrisumlem1  25178  dchrvmasumiflem1  25190  rpvmasum2  25201  dchrvmasumlem  25212  padicabv  25319  indispconn  31216  fnejoin1  32363  ptrecube  33409  poimirlem16  33425  poimirlem17  33426  poimirlem19  33428  poimirlem20  33429  fdc  33541  cdlemk40f  36207  sdrgacs  37771  blenn0  42367