Theorem ifbothda 4520

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 4487	. . . . . 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 4490	. . . . . 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 4481

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 4482

This theorem is referenced by:  ifboth  4521  resixpfo  8886  boxriin  8890  boxcutc  8891  suppr  9387  infpr  9420  cantnflem1  9610  ttukeylem5  10435  ttukeylem6  10436  bitsinv1lem  16380  bitsinv1  16381  smumullem  16431  hashgcdeq  16729  ramcl2lem  16949  acsfn  17594  tsrlemax  18521  odlem1  19476  gexlem1  19520  cyggex2  19838  dprdfeq0  19965  xrsdsreclb  21380  mplmon2  22028  evlslem1  22049  coe1tmmul2  22230  coe1tmmul  22231  ptcld  23569  xkopt  23611  stdbdxmet  24471  xrsxmet  24766  iccpnfcnv  24910  iccpnfhmeo  24911  xrhmeo  24912  dvcobr  25917  dvcobrOLD  25918  mdegle0  26050  dvradcnv  26398  psercnlem1  26403  psercn  26404  logtayl  26637  efrlim  26947  efrlimOLD  26948  lgamgulmlem5  27011  musum  27169  dchrmullid  27231  dchrsum2  27247  sumdchr2  27249  dchrisum0flblem1  27487  dchrisum0flblem2  27488  rplogsum  27506  pntlemj  27582  eupth2lem1  30305  eulerpathpr  30327  ifeqeqx  32628  sgn3da  32925  elrgspnlem2  33336  elrgspnlem3  33337  mplmulmvr  33715  esplyfv  33746  esplyfval3  33748  xrge0iifcnv  34110  xrge0iifhom  34114  esumpinfval  34250  dstfrvunirn  34652  plymulx0  34724  signswn0  34737  signswch  34738  lpadmax  34859  lpadright  34861  fnejoin2  36582  poimirlem16  37876  poimirlem17  37877  poimirlem19  37879  poimirlem20  37880  poimirlem24  37884  cnambfre  37908  itg2addnclem  37911  itg2addnclem3  37913  itg2addnc  37914  itg2gt0cn  37915  ftc1anclem7  37939  ftc1anclem8  37940  ftc1anc  37941  sticksstones10  42514  sticksstones12a  42516  aks6d1c6lem3  42531  kelac1  43409  discsubc  49412  iinfconstbas  49414  discthing  49809