Theorem sylan2br 282

Description: A syllogism inference. (Contributed by NM, 21-Apr-1994.)

Hypotheses

Ref	Expression
sylan2br.1	⊢ (𝜒 ↔ 𝜑)
sylan2br.2	⊢ ((𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
sylan2br	⊢ ((𝜓 ∧ 𝜑) → 𝜃)

Proof of Theorem sylan2br

Step	Hyp	Ref	Expression
1		sylan2br.1	. . 3 ⊢ (𝜒 ↔ 𝜑)
2	1	biimpri 131	. 2 ⊢ (𝜑 → 𝜒)
3		sylan2br.2	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
4	2, 3	sylan2 280	1 ⊢ ((𝜓 ∧ 𝜑) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 102   ↔ wb 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  syl2anbr  286  xordc1  1327  imainss  4813  xpexr2m  4838  funeu2  5006  imadiflem  5058  fnop  5082  ssimaex  5328  isosolem  5564  acexmidlem2  5610  fnovex  5639  cnvoprab  5956  smores3  6012  freccllem  6121  riinerm  6317  enq0sym  6935  peano5nnnn  7371  axcaucvglemres  7378  uzind3  8792  xrltnsym  9195  0fz1  9391  iseqfcl  9793  iseqfclt  9794  iseqf1oleml  9837  expivallem  9855  expival  9856  exp1  9860  expp1  9861  resqrexlemf1  10337  resqrexlemfp1  10338  clim2iser  10619  clim2iser2  10620  iisermulc2  10622  iserile  10624  climserile  10627  isummolem3  10661  fisumss  10672  fisumcvg3  10676  gcd0id  10852  lcmgcd  10942  lcmdvds  10943  lcmid  10944  isprm2lem  10980