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 2766	. . . . 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 4490	. . . . . 6 ⊢ (¬ 𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐵)
10	9	eqcomd 2766	. . . . 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 4481

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 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-if 4482

This theorem is used by:  ifboth  4521  resixpfo  8942  boxriin  8946  boxcutc  8947  suppr  9442  infpr  9475  cantnflem1  9668  ttukeylem5  10563  ttukeylem6  10564  sgn3da  15222  bitsinv1lem  16579  bitsinv1  16580  smumullem  16630  hashgcdeq  16929  ramcl2lem  17149  acsfn  17795  tsrlemax  18722  odlem1  19711  gexlem1  19755  cyggex2  20073  dprdfeq0  20200  xrsdsreclb  21682  mplmon2  22332  evlslem1  22353  coe1tmmul2  22557  coe1tmmul  22558  ptcld  23894  xkopt  23936  stdbdxmet  24796  xrsxmet  25091  iccpnfcnv  25227  iccpnfhmeo  25228  xrhmeo  25229  dvcobr  26228  mdegle0  26357  plyn0mulidp  26566  dvradcnv  26712  psercnlem1  26716  psercn  26717  logtayl  26952  efrlim  27261  lgamgulmlem5  27324  musum  27482  dchrmullid  27543  dchrsum2  27559  sumdchr2  27561  dchrisum0flblem1  27799  dchrisum0flblem2  27800  rplogsum  27818  pntlemj  27894  eupth2lem1  30753  eulerpathpr  30775  ifeqeqx  33072  elrgspnlem2  33738  elrgspnlem3  33739  mplasclco  34082  mplmulmvr  34105  esplyfv  34136  esplyfval3  34138  xrge0iifcnv  34499  xrge0iifhom  34503  esumpinfval  34639  dstfrvunirn  35042  signswn0  35124  signswch  35125  lpadmax  35249  lpadright  35251  fnejoin2  37079  poimirlem16  38474  poimirlem17  38475  poimirlem19  38477  poimirlem20  38478  poimirlem24  38482  cnambfre  38506  itg2addnclem  38509  itg2addnclem3  38511  itg2addnc  38512  itg2gt0cn  38513  ftc1anclem7  38537  ftc1anclem8  38538  ftc1anc  38539  sticksstones10  43125  sticksstones12a  43127  aks6d1c6lem3  43142  kelac1  44008  discsubc  50094  iinfconstbas  50096  discthing  50491