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

Theorem ifbothda 4100
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 4069 . . . . . 6 (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴)
32eqcomd 2627 . . . . 5 (𝜑𝐴 = if(𝜑, 𝐴, 𝐵))
4 ifboth.1 . . . . 5 (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝜓𝜃))
53, 4syl 17 . . . 4 (𝜑 → (𝜓𝜃))
65adantl 482 . . 3 ((𝜂𝜑) → (𝜓𝜃))
71, 6mpbid 222 . 2 ((𝜂𝜑) → 𝜃)
8 ifbothda.4 . . 3 ((𝜂 ∧ ¬ 𝜑) → 𝜒)
9 iffalse 4072 . . . . . 6 𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐵)
109eqcomd 2627 . . . . 5 𝜑𝐵 = if(𝜑, 𝐴, 𝐵))
11 ifboth.2 . . . . 5 (𝐵 = if(𝜑, 𝐴, 𝐵) → (𝜒𝜃))
1210, 11syl 17 . . . 4 𝜑 → (𝜒𝜃))
1312adantl 482 . . 3 ((𝜂 ∧ ¬ 𝜑) → (𝜒𝜃))
148, 13mpbid 222 . 2 ((𝜂 ∧ ¬ 𝜑) → 𝜃)
157, 14pm2.61dan 831 1 (𝜂𝜃)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 384   = wceq 1480  ifcif 4063
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-if 4064
This theorem is referenced by:  ifboth  4101  resixpfo  7897  boxriin  7901  boxcutc  7902  suppr  8328  infpr  8360  cantnflem1  8537  ttukeylem5  9286  ttukeylem6  9287  bitsinv1lem  15094  bitsinv1  15095  smumullem  15145  hashgcdeq  15425  ramcl2lem  15644  acsfn  16248  tsrlemax  17148  odlem1  17882  gexlem1  17922  cyggex2  18226  dprdfeq0  18349  mplmon2  19421  evlslem1  19443  coe1tmmul2  19574  coe1tmmul  19575  xrsdsreclb  19721  ptcld  21335  xkopt  21377  stdbdxmet  22239  xrsxmet  22531  iccpnfcnv  22662  iccpnfhmeo  22663  xrhmeo  22664  dvcobr  23628  mdegle0  23754  dvradcnv  24092  psercnlem1  24096  psercn  24097  logtayl  24319  efrlim  24609  lgamgulmlem5  24672  musum  24830  dchrmulid2  24890  dchrsum2  24906  sumdchr2  24908  dchrisum0flblem1  25110  dchrisum0flblem2  25111  rplogsum  25129  pntlemj  25205  eupth2lem1  26957  eulerpathpr  26979  ifeqeqx  29226  xrge0iifcnv  29779  xrge0iifhom  29783  esumpinfval  29934  dstfrvunirn  30335  sgn3da  30402  plymulx0  30422  signswn0  30435  signswch  30436  fnejoin2  32033  poimirlem16  33084  poimirlem17  33085  poimirlem19  33087  poimirlem20  33088  poimirlem24  33092  cnambfre  33117  itg2addnclem  33120  itg2addnclem3  33122  itg2addnc  33123  itg2gt0cn  33124  ftc1anclem7  33150  ftc1anclem8  33151  ftc1anc  33152  kelac1  37140
  Copyright terms: Public domain W3C validator