Theorem ifbothda 4497

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

Step	Hyp	Ref	Expression
1		ifbothda.3	. . 3 ⊢ ((𝜂 ∧ 𝜑) → 𝜓)
2		iftrue 4465	. . . . . 6 ⊢ (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴)
3	2	eqcomd 2744	. . . . 5 ⊢ (𝜑 → 𝐴 = if(𝜑, 𝐴, 𝐵))
4		ifboth.1	. . . . 5 ⊢ (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝜓 ↔ 𝜃))
5	3, 4	syl 17	. . . 4 ⊢ (𝜑 → (𝜓 ↔ 𝜃))
6	5	adantl 482	. . 3 ⊢ ((𝜂 ∧ 𝜑) → (𝜓 ↔ 𝜃))
7	1, 6	mpbid 231	. 2 ⊢ ((𝜂 ∧ 𝜑) → 𝜃)
8		ifbothda.4	. . 3 ⊢ ((𝜂 ∧ ¬ 𝜑) → 𝜒)
9		iffalse 4468	. . . . . 6 ⊢ (¬ 𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐵)
10	9	eqcomd 2744	. . . . 5 ⊢ (¬ 𝜑 → 𝐵 = if(𝜑, 𝐴, 𝐵))
11		ifboth.2	. . . . 5 ⊢ (𝐵 = if(𝜑, 𝐴, 𝐵) → (𝜒 ↔ 𝜃))
12	10, 11	syl 17	. . . 4 ⊢ (¬ 𝜑 → (𝜒 ↔ 𝜃))
13	12	adantl 482	. . 3 ⊢ ((𝜂 ∧ ¬ 𝜑) → (𝜒 ↔ 𝜃))
14	8, 13	mpbid 231	. 2 ⊢ ((𝜂 ∧ ¬ 𝜑) → 𝜃)
15	7, 14	pm2.61dan 810	1 ⊢ (𝜂 → 𝜃)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1539  ifcif 4459

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-if 4460

This theorem is referenced by:  ifboth  4498  resixpfo  8724  boxriin  8728  boxcutc  8729  suppr  9230  infpr  9262  cantnflem1  9447  ttukeylem5  10269  ttukeylem6  10270  bitsinv1lem  16148  bitsinv1  16149  smumullem  16199  hashgcdeq  16490  ramcl2lem  16710  acsfn  17368  tsrlemax  18304  odlem1  19143  gexlem1  19184  cyggex2  19498  dprdfeq0  19625  xrsdsreclb  20645  mplmon2  21269  evlslem1  21292  coe1tmmul2  21447  coe1tmmul  21448  ptcld  22764  xkopt  22806  stdbdxmet  23671  xrsxmet  23972  iccpnfcnv  24107  iccpnfhmeo  24108  xrhmeo  24109  dvcobr  25110  mdegle0  25242  dvradcnv  25580  psercnlem1  25584  psercn  25585  logtayl  25815  efrlim  26119  lgamgulmlem5  26182  musum  26340  dchrmulid2  26400  dchrsum2  26416  sumdchr2  26418  dchrisum0flblem1  26656  dchrisum0flblem2  26657  rplogsum  26675  pntlemj  26751  eupth2lem1  28582  eulerpathpr  28604  ifeqeqx  30885  xrge0iifcnv  31883  xrge0iifhom  31887  esumpinfval  32041  dstfrvunirn  32441  sgn3da  32508  plymulx0  32526  signswn0  32539  signswch  32540  lpadmax  32662  lpadright  32664  fnejoin2  34558  poimirlem16  35793  poimirlem17  35794  poimirlem19  35796  poimirlem20  35797  poimirlem24  35801  cnambfre  35825  itg2addnclem  35828  itg2addnclem3  35830  itg2addnc  35831  itg2gt0cn  35832  ftc1anclem7  35856  ftc1anclem8  35857  ftc1anc  35858  sticksstones10  40111  sticksstones12a  40113  metakunt1  40125  metakunt2  40126  metakunt25  40149  kelac1  40888