Theorem ifbothda 4462

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 4431	. . . . . 6 ⊢ (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴)
3	2	eqcomd 2804	. . . . 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 4434	. . . . . 6 ⊢ (¬ 𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐵)
10	9	eqcomd 2804	. . . . 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 812	1 ⊢ (𝜂 → 𝜃)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-if 4426

This theorem is referenced by:  ifboth  4463  resixpfo  8483  boxriin  8487  boxcutc  8488  suppr  8919  infpr  8951  cantnflem1  9136  ttukeylem5  9924  ttukeylem6  9925  bitsinv1lem  15780  bitsinv1  15781  smumullem  15831  hashgcdeq  16116  ramcl2lem  16335  acsfn  16922  tsrlemax  17822  odlem1  18655  gexlem1  18696  cyggex2  19010  dprdfeq0  19137  xrsdsreclb  20138  mplmon2  20732  evlslem1  20754  coe1tmmul2  20905  coe1tmmul  20906  ptcld  22218  xkopt  22260  stdbdxmet  23122  xrsxmet  23414  iccpnfcnv  23549  iccpnfhmeo  23550  xrhmeo  23551  dvcobr  24549  mdegle0  24678  dvradcnv  25016  psercnlem1  25020  psercn  25021  logtayl  25251  efrlim  25555  lgamgulmlem5  25618  musum  25776  dchrmulid2  25836  dchrsum2  25852  sumdchr2  25854  dchrisum0flblem1  26092  dchrisum0flblem2  26093  rplogsum  26111  pntlemj  26187  eupth2lem1  28003  eulerpathpr  28025  ifeqeqx  30309  xrge0iifcnv  31286  xrge0iifhom  31290  esumpinfval  31442  dstfrvunirn  31842  sgn3da  31909  plymulx0  31927  signswn0  31940  signswch  31941  lpadmax  32063  lpadright  32065  fnejoin2  33830  poimirlem16  35073  poimirlem17  35074  poimirlem19  35076  poimirlem20  35077  poimirlem24  35081  cnambfre  35105  itg2addnclem  35108  itg2addnclem3  35110  itg2addnc  35111  itg2gt0cn  35112  ftc1anclem7  35136  ftc1anclem8  35137  ftc1anc  35138  metakunt1  39350  metakunt2  39351  metakunt25  39374  kelac1  40007