MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ifbieq2d Structured version   Visualization version   GIF version

Theorem ifbieq2d 4219
Description: Equivalence/equality deduction for conditional operators. (Contributed by Paul Chapman, 22-Jun-2011.)
Hypotheses
Ref Expression
ifbieq2d.1 (𝜑 → (𝜓𝜒))
ifbieq2d.2 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
ifbieq2d (𝜑 → if(𝜓, 𝐶, 𝐴) = if(𝜒, 𝐶, 𝐵))

Proof of Theorem ifbieq2d
StepHypRef Expression
1 ifbieq2d.1 . . 3 (𝜑 → (𝜓𝜒))
21ifbid 4216 . 2 (𝜑 → if(𝜓, 𝐶, 𝐴) = if(𝜒, 𝐶, 𝐴))
3 ifbieq2d.2 . . 3 (𝜑𝐴 = 𝐵)
43ifeq2d 4213 . 2 (𝜑 → if(𝜒, 𝐶, 𝐴) = if(𝜒, 𝐶, 𝐵))
52, 4eqtrd 2758 1 (𝜑 → if(𝜓, 𝐶, 𝐴) = if(𝜒, 𝐶, 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1596  ifcif 4194
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-rab 3023  df-v 3306  df-un 3685  df-if 4195
This theorem is referenced by:  tz7.44-2  7623  tz7.44-3  7624  oev  7714  cantnfp1lem1  8688  cantnfp1lem3  8690  fin23lem12  9266  fin23lem33  9280  axcc2  9372  ttukeylem3  9446  ttukey2g  9451  canthp1lem2  9588  canthp1  9589  xnegeq  12152  xaddval  12168  xmulval  12170  expval  12977  cshfn  13657  ofccat  13830  relexpsucnnr  13885  sgnval  13948  sadcp1  15300  smupp1  15325  gcdval  15341  gcdass  15387  lcmval  15428  lcmass  15450  lcmfval  15457  lcmf0val  15458  lcmfpr  15463  iserodd  15663  pcval  15672  vdwlem6  15813  ramub1lem2  15854  ramcl  15856  mulgval  17665  symgextfv  17959  symgfixfo  17980  odval  18074  submod  18105  gexval  18114  znval  20006  fvmptnn04if  20777  cpmadumatpoly  20811  cayleyhamilton  20818  cayleyhamiltonALT  20819  ptcmplem2  21979  iccpnfhmeo  22866  pcopt  22943  ioombl1  23451  ioorval  23463  uniioombllem6  23477  itg1addlem3  23585  itg2uba  23630  limcfval  23756  limcmpt  23767  limcco  23777  dvcobr  23829  ig1pval  24052  abelthlem9  24314  logtayllem  24525  logtayl  24526  leibpilem2  24788  rlimcnp2  24813  efrlim  24816  igamval  24893  muval  24978  lgsval  25146  lgsfval  25147  lgsval2lem  25152  rpvmasum2  25321  padicval  25426  padicabv  25439  axlowdimlem15  25956  axlowdim  25961  eupth2lem3lem3  27303  eupth2  27312  eucrct2eupth  27318  sgnsv  29957  sgnsval  29958  psgnfzto1stlem  30080  madjusmdetlem2  30124  madjusmdet  30127  xrge0iifcv  30210  xrge0iifhom  30213  xrge0tmdOLD  30221  xrge0tmd  30222  signspval  30859  rdgprc0  31925  dfrdg2  31927  dfrdg4  32285  csbrdgg  33407  finxpeq1  33455  finxpreclem3  33462  poimirlem1  33642  poimirlem7  33648  poimirlem10  33651  poimirlem11  33652  itg2addnclem  33693  itg2addnclem3  33695  itg2addnc  33696  fdc  33773  heiborlem4  33845  heiborlem6  33847  heiborlem10  33851  mapdhval  37432  hdmap1fval  37505  hdmap1vallem  37506  hdmap1val  37507  hdmap1cbv  37511  irrapxlem4  37808  clsk1indlem0  38758  clsk1indlem2  38759  clsk1indlem3  38760  clsk1indlem4  38761  clsk1indlem1  38762  dirkerval2  40731  dirkeritg  40739  dirkercncf  40744  fourierdlem29  40773  fourierdlem37  40781  fourierdlem62  40805  fourierdlem79  40822  fourierdlem81  40824  fourierdlem82  40825  fourierdlem92  40835  fourierdlem96  40839  fourierdlem97  40840  fourierdlem98  40841  fourierdlem99  40842  fourierdlem105  40848  fourierdlem108  40851  fourierdlem110  40853  fourierdlem112  40855  fourierdlem113  40856  fouriersw  40868  etransclem24  40895  etransclem25  40896  etransclem31  40902  etransclem35  40906  etransclem37  40908  sge0val  41003  nnfoctbdjlem  41092  nnfoctbdj  41093  ovnval  41178  ovnval2  41182  ovnval2b  41189  hsphoif  41213  hoidmvval  41214  hsphoival  41216  hoidmv1lelem1  41228  hoidmv1lelem2  41229  hoidmv1lelem3  41230  hoidmv1le  41231  ovnhoi  41240  hoidifhspval  41245  hspmbllem2  41264  ovnsubadd2  41283  blenval  42792
  Copyright terms: Public domain W3C validator