Theorem ifbothda 4529

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 4497	. . . . . 6 ⊢ (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴)
3	2	eqcomd 2737	. . . . 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 4500	. . . . . 6 ⊢ (¬ 𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐵)
10	9	eqcomd 2737	. . . . 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 811	1 ⊢ (𝜂 → 𝜃)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-if 4492

This theorem is referenced by:  ifboth  4530  resixpfo  8881  boxriin  8885  boxcutc  8886  suppr  9416  infpr  9448  cantnflem1  9634  ttukeylem5  10458  ttukeylem6  10459  bitsinv1lem  16332  bitsinv1  16333  smumullem  16383  hashgcdeq  16672  ramcl2lem  16892  acsfn  17553  tsrlemax  18489  odlem1  19331  gexlem1  19375  cyggex2  19688  dprdfeq0  19815  xrsdsreclb  20881  mplmon2  21506  evlslem1  21529  coe1tmmul2  21684  coe1tmmul  21685  ptcld  23001  xkopt  23043  stdbdxmet  23908  xrsxmet  24209  iccpnfcnv  24344  iccpnfhmeo  24345  xrhmeo  24346  dvcobr  25347  mdegle0  25479  dvradcnv  25817  psercnlem1  25821  psercn  25822  logtayl  26052  efrlim  26356  lgamgulmlem5  26419  musum  26577  dchrmullid  26637  dchrsum2  26653  sumdchr2  26655  dchrisum0flblem1  26893  dchrisum0flblem2  26894  rplogsum  26912  pntlemj  26988  eupth2lem1  29225  eulerpathpr  29247  ifeqeqx  31528  xrge0iifcnv  32603  xrge0iifhom  32607  esumpinfval  32761  dstfrvunirn  33163  sgn3da  33230  plymulx0  33248  signswn0  33261  signswch  33262  lpadmax  33384  lpadright  33386  fnejoin2  34917  poimirlem16  36167  poimirlem17  36168  poimirlem19  36170  poimirlem20  36171  poimirlem24  36175  cnambfre  36199  itg2addnclem  36202  itg2addnclem3  36204  itg2addnc  36205  itg2gt0cn  36206  ftc1anclem7  36230  ftc1anclem8  36231  ftc1anc  36232  sticksstones10  40636  sticksstones12a  40638  metakunt1  40650  metakunt2  40651  metakunt25  40674  kelac1  41448