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  19663  gexlem1  19707  cyggex2  20025  dprdfeq0  20152  xrsdsreclb  21628  mplmon2  22278  evlslem1  22299  coe1tmmul2  22503  coe1tmmul  22504  ptcld  23840  xkopt  23882  stdbdxmet  24742  xrsxmet  25037  iccpnfcnv  25173  iccpnfhmeo  25174  xrhmeo  25175  dvcobr  26175  mdegle0  26304  plyn0mulidp  26512  dvradcnv  26654  psercnlem1  26658  psercn  26659  logtayl  26895  efrlim  27204  lgamgulmlem5  27267  musum  27425  dchrmullid  27486  dchrsum2  27502  sumdchr2  27504  dchrisum0flblem1  27742  dchrisum0flblem2  27743  rplogsum  27761  pntlemj  27837  eupth2lem1  30684  eulerpathpr  30706  ifeqeqx  33003  elrgspnlem2  33670  elrgspnlem3  33671  mplasclco  34013  mplmulmvr  34036  esplyfv  34067  esplyfval3  34069  xrge0iifcnv  34430  xrge0iifhom  34434  esumpinfval  34570  dstfrvunirn  34973  signswn0  35055  signswch  35056  lpadmax  35180  lpadright  35182  fnejoin2  36975  poimirlem16  38372  poimirlem17  38373  poimirlem19  38375  poimirlem20  38376  poimirlem24  38380  cnambfre  38404  itg2addnclem  38407  itg2addnclem3  38409  itg2addnc  38410  itg2gt0cn  38411  ftc1anclem7  38435  ftc1anclem8  38436  ftc1anc  38437  sticksstones10  43008  sticksstones12a  43010  aks6d1c6lem3  43025  kelac1  43891  discsubc  49977  iinfconstbas  49979  discthing  50374