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  1325  imainss  4769  xpexr2m  4792  funeu2  4957  imadiflem  5009  fnop  5033  ssimaex  5266  isosolem  5494  acexmidlem2  5540  fnovex  5569  cnvoprab  5886  smores3  5942  freccllem  6051  riinerm  6245  enq0sym  6684  peano5nnnn  7120  axcaucvglemres  7127  uzind3  8541  xrltnsym  8944  0fz1  9140  iseqfcl  9535  iseqfclt  9536  expivallem  9574  expival  9575  exp1  9579  expp1  9580  resqrexlemf1  10032  resqrexlemfp1  10033  clim2iser  10313  clim2iser2  10314  iisermulc2  10316  iserile  10318  climserile  10321  gcd0id  10514  lcmgcd  10604  lcmdvds  10605  lcmid  10606  isprm2lem  10642