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 4473	. . . . . 6 ⊢ (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴)
3	2	eqcomd 2743	. . . . 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 4476	. . . . . 6 ⊢ (¬ 𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐵)
10	9	eqcomd 2743	. . . . 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 813	1 ⊢ (𝜂 → 𝜃)

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

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-if 4468

This theorem is referenced by:  ifboth  4507  resixpfo  8884  boxriin  8888  boxcutc  8889  suppr  9385  infpr  9418  cantnflem1  9610  ttukeylem5  10435  ttukeylem6  10436  bitsinv1lem  16410  bitsinv1  16411  smumullem  16461  hashgcdeq  16760  ramcl2lem  16980  acsfn  17625  tsrlemax  18552  odlem1  19510  gexlem1  19554  cyggex2  19872  dprdfeq0  19999  xrsdsreclb  21394  mplmon2  22039  evlslem1  22060  coe1tmmul2  22241  coe1tmmul  22242  ptcld  23578  xkopt  23620  stdbdxmet  24480  xrsxmet  24775  iccpnfcnv  24911  iccpnfhmeo  24912  xrhmeo  24913  dvcobr  25913  mdegle0  26042  dvradcnv  26386  psercnlem1  26390  psercn  26391  logtayl  26624  efrlim  26933  lgamgulmlem5  26996  musum  27154  dchrmullid  27215  dchrsum2  27231  sumdchr2  27233  dchrisum0flblem1  27471  dchrisum0flblem2  27472  rplogsum  27490  pntlemj  27566  eupth2lem1  30288  eulerpathpr  30310  ifeqeqx  32612  sgn3da  32907  elrgspnlem2  33304  elrgspnlem3  33305  mplmulmvr  33683  esplyfv  33714  esplyfval3  33716  xrge0iifcnv  34077  xrge0iifhom  34081  esumpinfval  34217  dstfrvunirn  34619  plymulx0  34691  signswn0  34704  signswch  34705  lpadmax  34826  lpadright  34828  fnejoin2  36551  poimirlem16  37957  poimirlem17  37958  poimirlem19  37960  poimirlem20  37961  poimirlem24  37965  cnambfre  37989  itg2addnclem  37992  itg2addnclem3  37994  itg2addnc  37995  itg2gt0cn  37996  ftc1anclem7  38020  ftc1anclem8  38021  ftc1anc  38022  sticksstones10  42594  sticksstones12a  42596  aks6d1c6lem3  42611  kelac1  43491  discsubc  49533  iinfconstbas  49535  discthing  49930