Theorem ifbothda 4272

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 197   ∧ wa 383   = wceq 1634  ifcif 4235

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1873  ax-4 1888  ax-5 1994  ax-6 2060  ax-7 2096  ax-9 2157  ax-10 2177  ax-11 2193  ax-12 2206  ax-ext 2754

This theorem depends on definitions:  df-bi 198  df-an 384  df-or 864  df-tru 1637  df-ex 1856  df-nf 1861  df-sb 2053  df-clab 2761  df-cleq 2767  df-clel 2770  df-if 4236

This theorem is referenced by:  ifboth  4273  resixpfo  8121  boxriin  8125  boxcutc  8126  suppr  8554  infpr  8586  cantnflem1  8771  ttukeylem5  9558  ttukeylem6  9559  bitsinv1lem  15392  bitsinv1  15393  smumullem  15443  hashgcdeq  15721  ramcl2lem  15940  acsfn  16547  tsrlemax  17448  odlem1  18181  gexlem1  18221  cyggex2  18525  dprdfeq0  18649  mplmon2  19728  evlslem1  19750  coe1tmmul2  19881  coe1tmmul  19882  xrsdsreclb  20028  ptcld  21657  xkopt  21699  stdbdxmet  22560  xrsxmet  22852  iccpnfcnv  22983  iccpnfhmeo  22984  xrhmeo  22985  dvcobr  23950  mdegle0  24078  dvradcnv  24416  psercnlem1  24420  psercn  24421  logtayl  24648  efrlim  24938  lgamgulmlem5  25001  musum  25159  dchrmulid2  25219  dchrsum2  25235  sumdchr2  25237  dchrisum0flblem1  25439  dchrisum0flblem2  25440  rplogsum  25458  pntlemj  25534  eupth2lem1  27419  eulerpathpr  27441  ifeqeqx  29716  xrge0iifcnv  30336  xrge0iifhom  30340  esumpinfval  30492  dstfrvunirn  30893  sgn3da  30960  plymulx0  30981  signswn0  30994  signswch  30995  fnejoin2  32718  poimirlem16  33775  poimirlem17  33776  poimirlem19  33778  poimirlem20  33779  poimirlem24  33783  cnambfre  33807  itg2addnclem  33810  itg2addnclem3  33812  itg2addnc  33813  itg2gt0cn  33814  ftc1anclem7  33840  ftc1anclem8  33841  ftc1anc  33842  kelac1  38174