Theorem ifbothda 4525

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1569  ifcif 4486

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-if 4487

This theorem is used by:  ifboth  4526  resixpfo  8932  boxriin  8936  boxcutc  8937  suppr  9430  infpr  9463  cantnflem1  9656  ttukeylem5  10503  ttukeylem6  10504  sgn3da  15145  bitsinv1lem  16505  bitsinv1  16506  smumullem  16556  hashgcdeq  16855  ramcl2lem  17075  acsfn  17721  tsrlemax  18648  odlem1  19611  gexlem1  19655  cyggex2  19973  dprdfeq0  20100  xrsdsreclb  21575  mplmon2  22223  evlslem1  22244  coe1tmmul2  22448  coe1tmmul  22449  ptcld  23781  xkopt  23823  stdbdxmet  24683  xrsxmet  24978  iccpnfcnv  25114  iccpnfhmeo  25115  xrhmeo  25116  dvcobr  26116  mdegle0  26245  plyn0mulidp  26453  dvradcnv  26595  psercnlem1  26599  psercn  26600  logtayl  26836  efrlim  27145  lgamgulmlem5  27208  musum  27366  dchrmullid  27427  dchrsum2  27443  sumdchr2  27445  dchrisum0flblem1  27683  dchrisum0flblem2  27684  rplogsum  27702  pntlemj  27778  eupth2lem1  30580  eulerpathpr  30602  ifeqeqx  32899  elrgspnlem2  33572  elrgspnlem3  33573  mplasclco  33915  mplmulmvr  33938  esplyfv  33969  esplyfval3  33971  xrge0iifcnv  34332  xrge0iifhom  34336  esumpinfval  34472  dstfrvunirn  34874  signswn0  34956  signswch  34957  lpadmax  35081  lpadright  35083  fnejoin2  36908  poimirlem16  38315  poimirlem17  38316  poimirlem19  38318  poimirlem20  38319  poimirlem24  38323  cnambfre  38347  itg2addnclem  38350  itg2addnclem3  38352  itg2addnc  38353  itg2gt0cn  38354  ftc1anclem7  38378  ftc1anclem8  38379  ftc1anc  38380  sticksstones10  42950  sticksstones12a  42952  aks6d1c6lem3  42967  kelac1  43818  discsubc  49870  iinfconstbas  49872  discthing  50267