Theorem ifbothda 4344

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 198   ∧ wa 386   = wceq 1601  ifcif 4307

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-12 2163  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-if 4308

This theorem is referenced by:  ifboth  4345  resixpfo  8232  boxriin  8236  boxcutc  8237  suppr  8665  infpr  8697  cantnflem1  8883  ttukeylem5  9670  ttukeylem6  9671  bitsinv1lem  15569  bitsinv1  15570  smumullem  15620  hashgcdeq  15898  ramcl2lem  16117  acsfn  16705  tsrlemax  17606  odlem1  18338  gexlem1  18378  cyggex2  18684  dprdfeq0  18808  mplmon2  19889  evlslem1  19911  coe1tmmul2  20042  coe1tmmul  20043  xrsdsreclb  20189  ptcld  21825  xkopt  21867  stdbdxmet  22728  xrsxmet  23020  iccpnfcnv  23151  iccpnfhmeo  23152  xrhmeo  23153  dvcobr  24146  mdegle0  24274  dvradcnv  24612  psercnlem1  24616  psercn  24617  logtayl  24843  efrlim  25148  lgamgulmlem5  25211  musum  25369  dchrmulid2  25429  dchrsum2  25445  sumdchr2  25447  dchrisum0flblem1  25649  dchrisum0flblem2  25650  rplogsum  25668  pntlemj  25744  eupth2lem1  27622  eulerpathpr  27644  ifeqeqx  29924  xrge0iifcnv  30577  xrge0iifhom  30581  esumpinfval  30733  dstfrvunirn  31135  sgn3da  31202  plymulx0  31224  signswn0  31237  signswch  31238  fnejoin2  32952  poimirlem16  34051  poimirlem17  34052  poimirlem19  34054  poimirlem20  34055  poimirlem24  34059  cnambfre  34083  itg2addnclem  34086  itg2addnclem3  34088  itg2addnc  34089  itg2gt0cn  34090  ftc1anclem7  34116  ftc1anclem8  34117  ftc1anc  34118  kelac1  38592