Theorem ifbothda 4494

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-if 4457

This theorem is referenced by:  ifboth  4495  resixpfo  8682  boxriin  8686  boxcutc  8687  suppr  9160  infpr  9192  cantnflem1  9377  ttukeylem5  10200  ttukeylem6  10201  bitsinv1lem  16076  bitsinv1  16077  smumullem  16127  hashgcdeq  16418  ramcl2lem  16638  acsfn  17285  tsrlemax  18219  odlem1  19058  gexlem1  19099  cyggex2  19413  dprdfeq0  19540  xrsdsreclb  20557  mplmon2  21179  evlslem1  21202  coe1tmmul2  21357  coe1tmmul  21358  ptcld  22672  xkopt  22714  stdbdxmet  23577  xrsxmet  23878  iccpnfcnv  24013  iccpnfhmeo  24014  xrhmeo  24015  dvcobr  25015  mdegle0  25147  dvradcnv  25485  psercnlem1  25489  psercn  25490  logtayl  25720  efrlim  26024  lgamgulmlem5  26087  musum  26245  dchrmulid2  26305  dchrsum2  26321  sumdchr2  26323  dchrisum0flblem1  26561  dchrisum0flblem2  26562  rplogsum  26580  pntlemj  26656  eupth2lem1  28483  eulerpathpr  28505  ifeqeqx  30786  xrge0iifcnv  31785  xrge0iifhom  31789  esumpinfval  31941  dstfrvunirn  32341  sgn3da  32408  plymulx0  32426  signswn0  32439  signswch  32440  lpadmax  32562  lpadright  32564  fnejoin2  34485  poimirlem16  35720  poimirlem17  35721  poimirlem19  35723  poimirlem20  35724  poimirlem24  35728  cnambfre  35752  itg2addnclem  35755  itg2addnclem3  35757  itg2addnc  35758  itg2gt0cn  35759  ftc1anclem7  35783  ftc1anclem8  35784  ftc1anc  35785  sticksstones10  40039  sticksstones12a  40041  metakunt1  40053  metakunt2  40054  metakunt25  40077  kelac1  40804