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

Theorem ifbothda 4262
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 4231 . . . . . 6 (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴)
32eqcomd 2777 . . . . 5 (𝜑𝐴 = if(𝜑, 𝐴, 𝐵))
4 ifboth.1 . . . . 5 (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝜓𝜃))
53, 4syl 17 . . . 4 (𝜑 → (𝜓𝜃))
65adantl 467 . . 3 ((𝜂𝜑) → (𝜓𝜃))
71, 6mpbid 222 . 2 ((𝜂𝜑) → 𝜃)
8 ifbothda.4 . . 3 ((𝜂 ∧ ¬ 𝜑) → 𝜒)
9 iffalse 4234 . . . . . 6 𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐵)
109eqcomd 2777 . . . . 5 𝜑𝐵 = if(𝜑, 𝐴, 𝐵))
11 ifboth.2 . . . . 5 (𝐵 = if(𝜑, 𝐴, 𝐵) → (𝜒𝜃))
1210, 11syl 17 . . . 4 𝜑 → (𝜒𝜃))
1312adantl 467 . . 3 ((𝜂 ∧ ¬ 𝜑) → (𝜒𝜃))
148, 13mpbid 222 . 2 ((𝜂 ∧ ¬ 𝜑) → 𝜃)
157, 14pm2.61dan 796 1 (𝜂𝜃)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 382   = wceq 1631  ifcif 4225
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-if 4226
This theorem is referenced by:  ifboth  4263  resixpfo  8100  boxriin  8104  boxcutc  8105  suppr  8533  infpr  8565  cantnflem1  8750  ttukeylem5  9537  ttukeylem6  9538  bitsinv1lem  15371  bitsinv1  15372  smumullem  15422  hashgcdeq  15701  ramcl2lem  15920  acsfn  16527  tsrlemax  17428  odlem1  18161  gexlem1  18201  cyggex2  18505  dprdfeq0  18629  mplmon2  19708  evlslem1  19730  coe1tmmul2  19861  coe1tmmul  19862  xrsdsreclb  20008  ptcld  21637  xkopt  21679  stdbdxmet  22540  xrsxmet  22832  iccpnfcnv  22963  iccpnfhmeo  22964  xrhmeo  22965  dvcobr  23929  mdegle0  24057  dvradcnv  24395  psercnlem1  24399  psercn  24400  logtayl  24627  efrlim  24917  lgamgulmlem5  24980  musum  25138  dchrmulid2  25198  dchrsum2  25214  sumdchr2  25216  dchrisum0flblem1  25418  dchrisum0flblem2  25419  rplogsum  25437  pntlemj  25513  eupth2lem1  27398  eulerpathpr  27420  ifeqeqx  29699  xrge0iifcnv  30319  xrge0iifhom  30323  esumpinfval  30475  dstfrvunirn  30876  sgn3da  30943  plymulx0  30964  signswn0  30977  signswch  30978  fnejoin2  32701  poimirlem16  33758  poimirlem17  33759  poimirlem19  33761  poimirlem20  33762  poimirlem24  33766  cnambfre  33790  itg2addnclem  33793  itg2addnclem3  33795  itg2addnc  33796  itg2gt0cn  33797  ftc1anclem7  33823  ftc1anclem8  33824  ftc1anc  33825  kelac1  38159
  Copyright terms: Public domain W3C validator