Theorem sylan2br 286

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 284	1 ⊢ ((𝜓 ∧ 𝜑) → 𝜃)

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  syl2anbr  290  xordc1  1371  imainss  4949  xpexr2m  4975  funeu2  5144  imadiflem  5197  fnop  5221  ssimaex  5475  isosolem  5718  acexmidlem2  5764  fnovex  5797  cnvoprab  6124  smores3  6183  freccllem  6292  riinerm  6495  enq0sym  7233  peano5nnnn  7693  axcaucvglemres  7700  uzind3  9157  xrltnsym  9572  xsubge0  9657  0fz1  9818  seqf  10227  seq3f1oleml  10269  exp1  10292  expp1  10293  resqrexlemf1  10773  resqrexlemfp1  10774  clim2ser  11099  clim2ser2  11100  isermulc2  11102  summodclem3  11142  fisumss  11154  fsum3cvg3  11158  iserabs  11237  isumshft  11252  isumsplit  11253  geoisum1  11281  geoisum1c  11282  cvgratnnlemnexp  11286  cvgratz  11294  mertenslem2  11298  clim2prod  11301  clim2divap  11302  effsumlt  11387  efgt1p  11391  gcd0id  11656  lcmgcd  11748  lcmdvds  11749  lcmid  11750  isprm2lem  11786  ennnfonelemjn  11904  neipsm  12312  xmetpsmet  12527  comet  12657  metrest  12664  expcncf  12750  exmid1stab  13184  cvgcmp2nlemabs  13216