Theorem ifbothda 4565

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-if 4528

This theorem is referenced by:  ifboth  4566  resixpfo  8932  boxriin  8936  boxcutc  8937  suppr  9468  infpr  9500  cantnflem1  9686  ttukeylem5  10510  ttukeylem6  10511  bitsinv1lem  16386  bitsinv1  16387  smumullem  16437  hashgcdeq  16726  ramcl2lem  16946  acsfn  17607  tsrlemax  18543  odlem1  19444  gexlem1  19488  cyggex2  19806  dprdfeq0  19933  xrsdsreclb  21192  mplmon2  21841  evlslem1  21864  coe1tmmul2  22018  coe1tmmul  22019  ptcld  23337  xkopt  23379  stdbdxmet  24244  xrsxmet  24545  iccpnfcnv  24689  iccpnfhmeo  24690  xrhmeo  24691  dvcobr  25697  dvcobrOLD  25698  mdegle0  25830  dvradcnv  26169  psercnlem1  26173  psercn  26174  logtayl  26404  efrlim  26710  lgamgulmlem5  26773  musum  26931  dchrmullid  26991  dchrsum2  27007  sumdchr2  27009  dchrisum0flblem1  27247  dchrisum0flblem2  27248  rplogsum  27266  pntlemj  27342  eupth2lem1  29738  eulerpathpr  29760  ifeqeqx  32041  xrge0iifcnv  33211  xrge0iifhom  33215  esumpinfval  33369  dstfrvunirn  33771  sgn3da  33838  plymulx0  33856  signswn0  33869  signswch  33870  lpadmax  33992  lpadright  33994  fnejoin2  35557  poimirlem16  36807  poimirlem17  36808  poimirlem19  36810  poimirlem20  36811  poimirlem24  36815  cnambfre  36839  itg2addnclem  36842  itg2addnclem3  36844  itg2addnc  36845  itg2gt0cn  36846  ftc1anclem7  36870  ftc1anclem8  36871  ftc1anc  36872  sticksstones10  41277  sticksstones12a  41279  metakunt1  41291  metakunt2  41292  metakunt25  41315  kelac1  42107