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  8888  boxriin  8892  boxcutc  8893  suppr  9389  infpr  9422  cantnflem1  9612  ttukeylem5  10437  ttukeylem6  10438  bitsinv1lem  16382  bitsinv1  16383  smumullem  16433  hashgcdeq  16731  ramcl2lem  16951  acsfn  17596  tsrlemax  18523  odlem1  19481  gexlem1  19525  cyggex2  19843  dprdfeq0  19970  xrsdsreclb  21385  mplmon2  22033  evlslem1  22054  coe1tmmul2  22235  coe1tmmul  22236  ptcld  23574  xkopt  23616  stdbdxmet  24476  xrsxmet  24771  iccpnfcnv  24915  iccpnfhmeo  24916  xrhmeo  24917  dvcobr  25922  dvcobrOLD  25923  mdegle0  26055  dvradcnv  26403  psercnlem1  26408  psercn  26409  logtayl  26642  efrlim  26952  efrlimOLD  26953  lgamgulmlem5  27016  musum  27174  dchrmullid  27236  dchrsum2  27252  sumdchr2  27254  dchrisum0flblem1  27492  dchrisum0flblem2  27493  rplogsum  27511  pntlemj  27587  eupth2lem1  30311  eulerpathpr  30333  ifeqeqx  32635  sgn3da  32932  elrgspnlem2  33343  elrgspnlem3  33344  mplmulmvr  33722  esplyfv  33753  esplyfval3  33755  xrge0iifcnv  34117  xrge0iifhom  34121  esumpinfval  34257  dstfrvunirn  34659  plymulx0  34731  signswn0  34744  signswch  34745  lpadmax  34866  lpadright  34868  fnejoin2  36591  poimirlem16  37916  poimirlem17  37917  poimirlem19  37919  poimirlem20  37920  poimirlem24  37924  cnambfre  37948  itg2addnclem  37951  itg2addnclem3  37953  itg2addnc  37954  itg2gt0cn  37955  ftc1anclem7  37979  ftc1anclem8  37980  ftc1anc  37981  sticksstones10  42554  sticksstones12a  42556  aks6d1c6lem3  42571  kelac1  43449  discsubc  49452  iinfconstbas  49454  discthing  49849