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

Theorem ifbothda 4561
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 4529 . . . . . 6 (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴)
32eqcomd 2732 . . . . 5 (𝜑𝐴 = if(𝜑, 𝐴, 𝐵))
4 ifboth.1 . . . . 5 (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝜓𝜃))
53, 4syl 17 . . . 4 (𝜑 → (𝜓𝜃))
65adantl 481 . . 3 ((𝜂𝜑) → (𝜓𝜃))
71, 6mpbid 231 . 2 ((𝜂𝜑) → 𝜃)
8 ifbothda.4 . . 3 ((𝜂 ∧ ¬ 𝜑) → 𝜒)
9 iffalse 4532 . . . . . 6 𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐵)
109eqcomd 2732 . . . . 5 𝜑𝐵 = if(𝜑, 𝐴, 𝐵))
11 ifboth.2 . . . . 5 (𝐵 = if(𝜑, 𝐴, 𝐵) → (𝜒𝜃))
1210, 11syl 17 . . . 4 𝜑 → (𝜒𝜃))
1312adantl 481 . . 3 ((𝜂 ∧ ¬ 𝜑) → (𝜒𝜃))
148, 13mpbid 231 . 2 ((𝜂 ∧ ¬ 𝜑) → 𝜃)
157, 14pm2.61dan 810 1 (𝜂𝜃)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 395   = wceq 1533  ifcif 4523
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 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2697
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-ex 1774  df-sb 2060  df-clab 2704  df-cleq 2718  df-clel 2804  df-if 4524
This theorem is referenced by:  ifboth  4562  resixpfo  8932  boxriin  8936  boxcutc  8937  suppr  9468  infpr  9500  cantnflem1  9686  ttukeylem5  10510  ttukeylem6  10511  bitsinv1lem  16389  bitsinv1  16390  smumullem  16440  hashgcdeq  16731  ramcl2lem  16951  acsfn  17612  tsrlemax  18551  odlem1  19455  gexlem1  19499  cyggex2  19817  dprdfeq0  19944  xrsdsreclb  21307  mplmon2  21964  evlslem1  21987  coe1tmmul2  22150  coe1tmmul  22151  ptcld  23472  xkopt  23514  stdbdxmet  24379  xrsxmet  24680  iccpnfcnv  24824  iccpnfhmeo  24825  xrhmeo  24826  dvcobr  25832  dvcobrOLD  25833  mdegle0  25968  dvradcnv  26312  psercnlem1  26317  psercn  26318  logtayl  26549  efrlim  26856  efrlimOLD  26857  lgamgulmlem5  26920  musum  27078  dchrmullid  27140  dchrsum2  27156  sumdchr2  27158  dchrisum0flblem1  27396  dchrisum0flblem2  27397  rplogsum  27415  pntlemj  27491  eupth2lem1  29980  eulerpathpr  30002  ifeqeqx  32283  xrge0iifcnv  33443  xrge0iifhom  33447  esumpinfval  33601  dstfrvunirn  34003  sgn3da  34070  plymulx0  34088  signswn0  34101  signswch  34102  lpadmax  34223  lpadright  34225  fnejoin2  35762  poimirlem16  37017  poimirlem17  37018  poimirlem19  37020  poimirlem20  37021  poimirlem24  37025  cnambfre  37049  itg2addnclem  37052  itg2addnclem3  37054  itg2addnc  37055  itg2gt0cn  37056  ftc1anclem7  37080  ftc1anclem8  37081  ftc1anc  37082  sticksstones10  41532  sticksstones12a  41534  metakunt1  41546  metakunt2  41547  metakunt25  41570  kelac1  42383
  Copyright terms: Public domain W3C validator