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

Theorem ifbothda 4525
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 4493 . . . . . 6 (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴)
32eqcomd 2743 . . . . 5 (𝜑𝐴 = if(𝜑, 𝐴, 𝐵))
4 ifboth.1 . . . . 5 (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝜓𝜃))
53, 4syl 17 . . . 4 (𝜑 → (𝜓𝜃))
65adantl 483 . . 3 ((𝜂𝜑) → (𝜓𝜃))
71, 6mpbid 231 . 2 ((𝜂𝜑) → 𝜃)
8 ifbothda.4 . . 3 ((𝜂 ∧ ¬ 𝜑) → 𝜒)
9 iffalse 4496 . . . . . 6 𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐵)
109eqcomd 2743 . . . . 5 𝜑𝐵 = if(𝜑, 𝐴, 𝐵))
11 ifboth.2 . . . . 5 (𝐵 = if(𝜑, 𝐴, 𝐵) → (𝜒𝜃))
1210, 11syl 17 . . . 4 𝜑 → (𝜒𝜃))
1312adantl 483 . . 3 ((𝜂 ∧ ¬ 𝜑) → (𝜒𝜃))
148, 13mpbid 231 . 2 ((𝜂 ∧ ¬ 𝜑) → 𝜃)
157, 14pm2.61dan 812 1 (𝜂𝜃)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 397   = wceq 1542  ifcif 4487
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-if 4488
This theorem is referenced by:  ifboth  4526  resixpfo  8875  boxriin  8879  boxcutc  8880  suppr  9408  infpr  9440  cantnflem1  9626  ttukeylem5  10450  ttukeylem6  10451  bitsinv1lem  16322  bitsinv1  16323  smumullem  16373  hashgcdeq  16662  ramcl2lem  16882  acsfn  17540  tsrlemax  18476  odlem1  19318  gexlem1  19362  cyggex2  19675  dprdfeq0  19802  xrsdsreclb  20847  mplmon2  21472  evlslem1  21495  coe1tmmul2  21650  coe1tmmul  21651  ptcld  22967  xkopt  23009  stdbdxmet  23874  xrsxmet  24175  iccpnfcnv  24310  iccpnfhmeo  24311  xrhmeo  24312  dvcobr  25313  mdegle0  25445  dvradcnv  25783  psercnlem1  25787  psercn  25788  logtayl  26018  efrlim  26322  lgamgulmlem5  26385  musum  26543  dchrmulid2  26603  dchrsum2  26619  sumdchr2  26621  dchrisum0flblem1  26859  dchrisum0flblem2  26860  rplogsum  26878  pntlemj  26954  eupth2lem1  29165  eulerpathpr  29187  ifeqeqx  31467  xrge0iifcnv  32517  xrge0iifhom  32521  esumpinfval  32675  dstfrvunirn  33077  sgn3da  33144  plymulx0  33162  signswn0  33175  signswch  33176  lpadmax  33298  lpadright  33300  fnejoin2  34844  poimirlem16  36097  poimirlem17  36098  poimirlem19  36100  poimirlem20  36101  poimirlem24  36105  cnambfre  36129  itg2addnclem  36132  itg2addnclem3  36134  itg2addnc  36135  itg2gt0cn  36136  ftc1anclem7  36160  ftc1anclem8  36161  ftc1anc  36162  sticksstones10  40566  sticksstones12a  40568  metakunt1  40580  metakunt2  40581  metakunt25  40604  kelac1  41393
  Copyright terms: Public domain W3C validator