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

Theorem ifbothda 4502
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 4471 . . . . . 6 (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴)
32eqcomd 2825 . . . . 5 (𝜑𝐴 = if(𝜑, 𝐴, 𝐵))
4 ifboth.1 . . . . 5 (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝜓𝜃))
53, 4syl 17 . . . 4 (𝜑 → (𝜓𝜃))
65adantl 484 . . 3 ((𝜂𝜑) → (𝜓𝜃))
71, 6mpbid 234 . 2 ((𝜂𝜑) → 𝜃)
8 ifbothda.4 . . 3 ((𝜂 ∧ ¬ 𝜑) → 𝜒)
9 iffalse 4474 . . . . . 6 𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐵)
109eqcomd 2825 . . . . 5 𝜑𝐵 = if(𝜑, 𝐴, 𝐵))
11 ifboth.2 . . . . 5 (𝐵 = if(𝜑, 𝐴, 𝐵) → (𝜒𝜃))
1210, 11syl 17 . . . 4 𝜑 → (𝜒𝜃))
1312adantl 484 . . 3 ((𝜂 ∧ ¬ 𝜑) → (𝜒𝜃))
148, 13mpbid 234 . 2 ((𝜂 ∧ ¬ 𝜑) → 𝜃)
157, 14pm2.61dan 811 1 (𝜂𝜃)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 208  wa 398   = wceq 1530  ifcif 4465
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-ext 2791
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-ex 1774  df-sb 2063  df-clab 2798  df-cleq 2812  df-clel 2891  df-if 4466
This theorem is referenced by:  ifboth  4503  resixpfo  8492  boxriin  8496  boxcutc  8497  suppr  8927  infpr  8959  cantnflem1  9144  ttukeylem5  9927  ttukeylem6  9928  bitsinv1lem  15782  bitsinv1  15783  smumullem  15833  hashgcdeq  16118  ramcl2lem  16337  acsfn  16922  tsrlemax  17822  odlem1  18655  gexlem1  18696  cyggex2  19009  dprdfeq0  19136  mplmon2  20265  evlslem1  20287  coe1tmmul2  20436  coe1tmmul  20437  xrsdsreclb  20584  ptcld  22213  xkopt  22255  stdbdxmet  23117  xrsxmet  23409  iccpnfcnv  23540  iccpnfhmeo  23541  xrhmeo  23542  dvcobr  24535  mdegle0  24663  dvradcnv  25001  psercnlem1  25005  psercn  25006  logtayl  25235  efrlim  25539  lgamgulmlem5  25602  musum  25760  dchrmulid2  25820  dchrsum2  25836  sumdchr2  25838  dchrisum0flblem1  26076  dchrisum0flblem2  26077  rplogsum  26095  pntlemj  26171  eupth2lem1  27989  eulerpathpr  28011  ifeqeqx  30289  xrge0iifcnv  31164  xrge0iifhom  31168  esumpinfval  31320  dstfrvunirn  31720  sgn3da  31787  plymulx0  31805  signswn0  31818  signswch  31819  lpadmax  31941  lpadright  31943  fnejoin2  33705  poimirlem16  34895  poimirlem17  34896  poimirlem19  34898  poimirlem20  34899  poimirlem24  34903  cnambfre  34927  itg2addnclem  34930  itg2addnclem3  34932  itg2addnc  34933  itg2gt0cn  34934  ftc1anclem7  34960  ftc1anclem8  34961  ftc1anc  34962  kelac1  39648
  Copyright terms: Public domain W3C validator