Theorem ifbothda 4449

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 4417	. . . . . 6 ⊢ (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴)
3	2	eqcomd 2744	. . . . 5 ⊢ (𝜑 → 𝐴 = if(𝜑, 𝐴, 𝐵))
4		ifboth.1	. . . . 5 ⊢ (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝜓 ↔ 𝜃))
5	3, 4	syl 17	. . . 4 ⊢ (𝜑 → (𝜓 ↔ 𝜃))
6	5	adantl 485	. . 3 ⊢ ((𝜂 ∧ 𝜑) → (𝜓 ↔ 𝜃))
7	1, 6	mpbid 235	. 2 ⊢ ((𝜂 ∧ 𝜑) → 𝜃)
8		ifbothda.4	. . 3 ⊢ ((𝜂 ∧ ¬ 𝜑) → 𝜒)
9		iffalse 4420	. . . . . 6 ⊢ (¬ 𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐵)
10	9	eqcomd 2744	. . . . 5 ⊢ (¬ 𝜑 → 𝐵 = if(𝜑, 𝐴, 𝐵))
11		ifboth.2	. . . . 5 ⊢ (𝐵 = if(𝜑, 𝐴, 𝐵) → (𝜒 ↔ 𝜃))
12	10, 11	syl 17	. . . 4 ⊢ (¬ 𝜑 → (𝜒 ↔ 𝜃))
13	12	adantl 485	. . 3 ⊢ ((𝜂 ∧ ¬ 𝜑) → (𝜒 ↔ 𝜃))
14	8, 13	mpbid 235	. 2 ⊢ ((𝜂 ∧ ¬ 𝜑) → 𝜃)
15	7, 14	pm2.61dan 813	1 ⊢ (𝜂 → 𝜃)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1542  ifcif 4411

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-ex 1787  df-sb 2074  df-clab 2717  df-cleq 2730  df-clel 2811  df-if 4412

This theorem is referenced by:  ifboth  4450  resixpfo  8539  boxriin  8543  boxcutc  8544  suppr  9001  infpr  9033  cantnflem1  9218  ttukeylem5  10006  ttukeylem6  10007  bitsinv1lem  15877  bitsinv1  15878  smumullem  15928  hashgcdeq  16219  ramcl2lem  16438  acsfn  17026  tsrlemax  17939  odlem1  18774  gexlem1  18815  cyggex2  19129  dprdfeq0  19256  xrsdsreclb  20257  mplmon2  20866  evlslem1  20889  coe1tmmul2  21044  coe1tmmul  21045  ptcld  22357  xkopt  22399  stdbdxmet  23261  xrsxmet  23554  iccpnfcnv  23689  iccpnfhmeo  23690  xrhmeo  23691  dvcobr  24690  mdegle0  24822  dvradcnv  25160  psercnlem1  25164  psercn  25165  logtayl  25395  efrlim  25699  lgamgulmlem5  25762  musum  25920  dchrmulid2  25980  dchrsum2  25996  sumdchr2  25998  dchrisum0flblem1  26236  dchrisum0flblem2  26237  rplogsum  26255  pntlemj  26331  eupth2lem1  28147  eulerpathpr  28169  ifeqeqx  30451  xrge0iifcnv  31447  xrge0iifhom  31451  esumpinfval  31603  dstfrvunirn  32003  sgn3da  32070  plymulx0  32088  signswn0  32101  signswch  32102  lpadmax  32224  lpadright  32226  fnejoin2  34188  poimirlem16  35405  poimirlem17  35406  poimirlem19  35408  poimirlem20  35409  poimirlem24  35413  cnambfre  35437  itg2addnclem  35440  itg2addnclem3  35442  itg2addnc  35443  itg2gt0cn  35444  ftc1anclem7  35468  ftc1anclem8  35469  ftc1anc  35470  metakunt1  39705  metakunt2  39706  metakunt25  39729  kelac1  40444