Theorem ifbothda 4515

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541  ifcif 4476

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-if 4477

This theorem is referenced by:  ifboth  4516  resixpfo  8869  boxriin  8873  boxcutc  8874  suppr  9366  infpr  9399  cantnflem1  9589  ttukeylem5  10414  ttukeylem6  10415  bitsinv1lem  16362  bitsinv1  16363  smumullem  16413  hashgcdeq  16711  ramcl2lem  16931  acsfn  17575  tsrlemax  18502  odlem1  19457  gexlem1  19501  cyggex2  19819  dprdfeq0  19946  xrsdsreclb  21360  mplmon2  22006  evlslem1  22027  coe1tmmul2  22200  coe1tmmul  22201  ptcld  23538  xkopt  23580  stdbdxmet  24440  xrsxmet  24735  iccpnfcnv  24879  iccpnfhmeo  24880  xrhmeo  24881  dvcobr  25886  dvcobrOLD  25887  mdegle0  26019  dvradcnv  26367  psercnlem1  26372  psercn  26373  logtayl  26606  efrlim  26916  efrlimOLD  26917  lgamgulmlem5  26980  musum  27138  dchrmullid  27200  dchrsum2  27216  sumdchr2  27218  dchrisum0flblem1  27456  dchrisum0flblem2  27457  rplogsum  27475  pntlemj  27551  eupth2lem1  30209  eulerpathpr  30231  ifeqeqx  32533  sgn3da  32828  elrgspnlem2  33221  elrgspnlem3  33222  esplyfv  33602  xrge0iifcnv  33957  xrge0iifhom  33961  esumpinfval  34097  dstfrvunirn  34499  plymulx0  34571  signswn0  34584  signswch  34585  lpadmax  34706  lpadright  34708  fnejoin2  36424  poimirlem16  37686  poimirlem17  37687  poimirlem19  37689  poimirlem20  37690  poimirlem24  37694  cnambfre  37718  itg2addnclem  37721  itg2addnclem3  37723  itg2addnc  37724  itg2gt0cn  37725  ftc1anclem7  37749  ftc1anclem8  37750  ftc1anc  37751  sticksstones10  42258  sticksstones12a  42260  aks6d1c6lem3  42275  kelac1  43170  discsubc  49179  iinfconstbas  49181  discthing  49576