Theorem ifbothda 4524

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 4491	. . . . . 6 ⊢ (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴)
3	2	eqcomd 2768	. . . . 5 ⊢ (𝜑 → 𝐴 = if(𝜑, 𝐴, 𝐵))
4		ifboth.1	. . . . 5 ⊢ (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝜓 ↔ 𝜃))
5	3, 4	syl 18	. . . 4 ⊢ (𝜑 → (𝜓 ↔ 𝜃))
6	5	adantl 487	. . 3 ⊢ ((𝜂 ∧ 𝜑) → (𝜓 ↔ 𝜃))
7	1, 6	mpbid 235	. 2 ⊢ ((𝜂 ∧ 𝜑) → 𝜃)
8		ifbothda.4	. . 3 ⊢ ((𝜂 ∧ ¬ 𝜑) → 𝜒)
9		iffalse 4494	. . . . . 6 ⊢ (¬ 𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐵)
10	9	eqcomd 2768	. . . . 5 ⊢ (¬ 𝜑 → 𝐵 = if(𝜑, 𝐴, 𝐵))
11		ifboth.2	. . . . 5 ⊢ (𝐵 = if(𝜑, 𝐴, 𝐵) → (𝜒 ↔ 𝜃))
12	10, 11	syl 18	. . . 4 ⊢ (¬ 𝜑 → (𝜒 ↔ 𝜃))
13	12	adantl 487	. . 3 ⊢ ((𝜂 ∧ ¬ 𝜑) → (𝜒 ↔ 𝜃))
14	8, 13	mpbid 235	. 2 ⊢ ((𝜂 ∧ ¬ 𝜑) → 𝜃)
15	7, 14	pm2.61dan 825	1 ⊢ (𝜂 → 𝜃)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570  ifcif 4485

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-if 4486

This theorem is used by:  ifboth  4525  resixpfo  8946  boxriin  8950  boxcutc  8951  suppr  9445  infpr  9478  cantnflem1  9671  ttukeylem5  10518  ttukeylem6  10519  sgn3da  15176  bitsinv1lem  16535  bitsinv1  16536  smumullem  16586  hashgcdeq  16885  ramcl2lem  17105  acsfn  17751  tsrlemax  18678  odlem1  19666  gexlem1  19710  cyggex2  20028  dprdfeq0  20155  xrsdsreclb  21631  mplmon2  22281  evlslem1  22302  coe1tmmul2  22506  coe1tmmul  22507  ptcld  23843  xkopt  23885  stdbdxmet  24745  xrsxmet  25040  iccpnfcnv  25176  iccpnfhmeo  25177  xrhmeo  25178  dvcobr  26178  mdegle0  26307  plyn0mulidp  26515  dvradcnv  26657  psercnlem1  26661  psercn  26662  logtayl  26898  efrlim  27207  lgamgulmlem5  27270  musum  27428  dchrmullid  27489  dchrsum2  27505  sumdchr2  27507  dchrisum0flblem1  27745  dchrisum0flblem2  27746  rplogsum  27764  pntlemj  27840  eupth2lem1  30699  eulerpathpr  30721  ifeqeqx  33018  elrgspnlem2  33685  elrgspnlem3  33686  mplasclco  34028  mplmulmvr  34051  esplyfv  34082  esplyfval3  34084  xrge0iifcnv  34445  xrge0iifhom  34449  esumpinfval  34585  dstfrvunirn  34988  signswn0  35070  signswch  35071  lpadmax  35195  lpadright  35197  fnejoin2  36990  poimirlem16  38387  poimirlem17  38388  poimirlem19  38390  poimirlem20  38391  poimirlem24  38395  cnambfre  38419  itg2addnclem  38422  itg2addnclem3  38424  itg2addnc  38425  itg2gt0cn  38426  ftc1anclem7  38450  ftc1anclem8  38451  ftc1anc  38452  sticksstones10  43023  sticksstones12a  43025  aks6d1c6lem3  43040  kelac1  43906  discsubc  49992  iinfconstbas  49994  discthing  50389