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

Theorem ifbothda 4449
Description: A wff 𝜃 containing a conditional operator is true when both of its cases are true. (Contributed by NM, 15-Feb-2015.)
Hypotheses
Ref Expression
ifboth.1 (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝜓𝜃))
ifboth.2 (𝐵 = if(𝜑, 𝐴, 𝐵) → (𝜒𝜃))
ifbothda.3 ((𝜂𝜑) → 𝜓)
ifbothda.4 ((𝜂 ∧ ¬ 𝜑) → 𝜒)
Assertion
Ref Expression
ifbothda (𝜂𝜃)

Proof of Theorem ifbothda
StepHypRef Expression
1 ifbothda.3 . . 3 ((𝜂𝜑) → 𝜓)
2 iftrue 4417 . . . . . 6 (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴)
32eqcomd 2744 . . . . 5 (𝜑𝐴 = if(𝜑, 𝐴, 𝐵))
4 ifboth.1 . . . . 5 (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝜓𝜃))
53, 4syl 17 . . . 4 (𝜑 → (𝜓𝜃))
65adantl 485 . . 3 ((𝜂𝜑) → (𝜓𝜃))
71, 6mpbid 235 . 2 ((𝜂𝜑) → 𝜃)
8 ifbothda.4 . . 3 ((𝜂 ∧ ¬ 𝜑) → 𝜒)
9 iffalse 4420 . . . . . 6 𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐵)
109eqcomd 2744 . . . . 5 𝜑𝐵 = if(𝜑, 𝐴, 𝐵))
11 ifboth.2 . . . . 5 (𝐵 = if(𝜑, 𝐴, 𝐵) → (𝜒𝜃))
1210, 11syl 17 . . . 4 𝜑 → (𝜒𝜃))
1312adantl 485 . . 3 ((𝜂 ∧ ¬ 𝜑) → (𝜒𝜃))
148, 13mpbid 235 . 2 ((𝜂 ∧ ¬ 𝜑) → 𝜃)
157, 14pm2.61dan 813 1 (𝜂𝜃)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399   = wceq 1542  ifcif 4411
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-ext 2710
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-ex 1787  df-sb 2074  df-clab 2717  df-cleq 2730  df-clel 2811  df-if 4412
This theorem is referenced by:  ifboth  4450  resixpfo  8539  boxriin  8543  boxcutc  8544  suppr  9001  infpr  9033  cantnflem1  9218  ttukeylem5  10006  ttukeylem6  10007  bitsinv1lem  15877  bitsinv1  15878  smumullem  15928  hashgcdeq  16219  ramcl2lem  16438  acsfn  17026  tsrlemax  17939  odlem1  18774  gexlem1  18815  cyggex2  19129  dprdfeq0  19256  xrsdsreclb  20257  mplmon2  20866  evlslem1  20889  coe1tmmul2  21044  coe1tmmul  21045  ptcld  22357  xkopt  22399  stdbdxmet  23261  xrsxmet  23554  iccpnfcnv  23689  iccpnfhmeo  23690  xrhmeo  23691  dvcobr  24690  mdegle0  24822  dvradcnv  25160  psercnlem1  25164  psercn  25165  logtayl  25395  efrlim  25699  lgamgulmlem5  25762  musum  25920  dchrmulid2  25980  dchrsum2  25996  sumdchr2  25998  dchrisum0flblem1  26236  dchrisum0flblem2  26237  rplogsum  26255  pntlemj  26331  eupth2lem1  28147  eulerpathpr  28169  ifeqeqx  30451  xrge0iifcnv  31447  xrge0iifhom  31451  esumpinfval  31603  dstfrvunirn  32003  sgn3da  32070  plymulx0  32088  signswn0  32101  signswch  32102  lpadmax  32224  lpadright  32226  fnejoin2  34188  poimirlem16  35405  poimirlem17  35406  poimirlem19  35408  poimirlem20  35409  poimirlem24  35413  cnambfre  35437  itg2addnclem  35440  itg2addnclem3  35442  itg2addnc  35443  itg2gt0cn  35444  ftc1anclem7  35468  ftc1anclem8  35469  ftc1anc  35470  metakunt1  39705  metakunt2  39706  metakunt25  39729  kelac1  40444
  Copyright terms: Public domain W3C validator