Theorem ifbothda 4506

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1537  ifcif 4469

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-ex 1781  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-if 4470

This theorem is referenced by:  ifboth  4507  resixpfo  8502  boxriin  8506  boxcutc  8507  suppr  8937  infpr  8969  cantnflem1  9154  ttukeylem5  9937  ttukeylem6  9938  bitsinv1lem  15792  bitsinv1  15793  smumullem  15843  hashgcdeq  16128  ramcl2lem  16347  acsfn  16932  tsrlemax  17832  odlem1  18665  gexlem1  18706  cyggex2  19019  dprdfeq0  19146  mplmon2  20275  evlslem1  20297  coe1tmmul2  20446  coe1tmmul  20447  xrsdsreclb  20594  ptcld  22223  xkopt  22265  stdbdxmet  23127  xrsxmet  23419  iccpnfcnv  23550  iccpnfhmeo  23551  xrhmeo  23552  dvcobr  24545  mdegle0  24673  dvradcnv  25011  psercnlem1  25015  psercn  25016  logtayl  25245  efrlim  25549  lgamgulmlem5  25612  musum  25770  dchrmulid2  25830  dchrsum2  25846  sumdchr2  25848  dchrisum0flblem1  26086  dchrisum0flblem2  26087  rplogsum  26105  pntlemj  26181  eupth2lem1  27999  eulerpathpr  28021  ifeqeqx  30299  xrge0iifcnv  31178  xrge0iifhom  31182  esumpinfval  31334  dstfrvunirn  31734  sgn3da  31801  plymulx0  31819  signswn0  31832  signswch  31833  lpadmax  31955  lpadright  31957  fnejoin2  33719  poimirlem16  34910  poimirlem17  34911  poimirlem19  34913  poimirlem20  34914  poimirlem24  34918  cnambfre  34942  itg2addnclem  34945  itg2addnclem3  34947  itg2addnc  34948  itg2gt0cn  34949  ftc1anclem7  34975  ftc1anclem8  34976  ftc1anc  34977  kelac1  39670