Theorem sylan2br 284

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 132	. 2 ⊢ (𝜑 → 𝜒)
3		sylan2br.2	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
4	2, 3	sylan2 282	1 ⊢ ((𝜓 ∧ 𝜑) → 𝜃)

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  syl2anbr  288  xordc1  1339  imainss  4890  xpexr2m  4916  funeu2  5085  imadiflem  5138  fnop  5162  ssimaex  5414  isosolem  5657  acexmidlem2  5703  fnovex  5736  cnvoprab  6061  smores3  6120  freccllem  6229  riinerm  6432  enq0sym  7141  peano5nnnn  7577  axcaucvglemres  7584  uzind3  9016  xrltnsym  9420  xsubge0  9505  0fz1  9666  seqf  10075  seq3f1oleml  10117  exp1  10140  expp1  10141  resqrexlemf1  10620  resqrexlemfp1  10621  clim2ser  10945  clim2ser2  10946  isermulc2  10948  summodclem3  10988  fisumss  11000  fsum3cvg3  11004  iserabs  11083  isumshft  11098  isumsplit  11099  geoisum1  11127  geoisum1c  11128  cvgratnnlemnexp  11132  cvgratz  11140  mertenslem2  11144  effsumlt  11196  efgt1p  11200  gcd0id  11462  lcmgcd  11552  lcmdvds  11553  lcmid  11554  isprm2lem  11590  ennnfonelemjn  11707  neipsm  12105  xmetpsmet  12297  comet  12427  metrest  12434  expcncf  12504  cvgcmp2nlemabs  12811