Theorem sylan2br 288

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

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

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  syl2anbr  292  xordc1  1404  exmid1stab  4242  imainss  5086  xpexr2m  5112  funeu2  5285  imadiflem  5338  fnop  5364  ssimaex  5625  isosolem  5874  acexmidlem2  5922  fnovex  5958  cnvoprab  6301  smores3  6360  freccllem  6469  riinerm  6676  pw1fin  6980  enq0sym  7518  peano5nnnn  7978  axcaucvglemres  7985  uzind3  9458  xrltnsym  9887  xsubge0  9975  0fz1  10139  seqf  10575  seq3f1oleml  10627  exp1  10656  expp1  10657  resqrexlemf1  11192  resqrexlemfp1  11193  clim2ser  11521  clim2ser2  11522  isermulc2  11524  summodclem3  11564  fisumss  11576  fsum3cvg3  11580  iserabs  11659  isumshft  11674  isumsplit  11675  geoisum1  11703  geoisum1c  11704  cvgratnnlemnexp  11708  cvgratz  11716  mertenslem2  11720  clim2prod  11723  clim2divap  11724  fprodseq  11767  prodssdc  11773  fprodssdc  11774  effsumlt  11876  efgt1p  11880  gcd0id  12173  nninfctlemfo  12234  lcmgcd  12273  lcmdvds  12274  lcmid  12275  isprm2lem  12311  pcmpt  12539  ennnfonelemjn  12646  issgrpd  13116  mulg1  13337  srglmhm  13627  srgrmhm  13628  ringlghm  13695  ringrghm  13696  neipsm  14498  xmetpsmet  14713  comet  14843  metrest  14850  expcncf  14953  lgscllem  15356  lgsdir2  15382  lgsdirnn0  15396  lgsdinn0  15397  cvgcmp2nlemabs  15789  nconstwlpolem  15822