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  1435  exmid1stab  4291  imainss  5143  xpexr2m  5169  funeu2  5343  imadiflem  5399  fnop  5425  ssimaex  5694  isosolem  5947  acexmidlem2  5997  fnovex  6033  cnvoprab  6378  smores3  6437  freccllem  6546  riinerm  6753  pw1fin  7068  enq0sym  7615  peano5nnnn  8075  axcaucvglemres  8082  uzind3  9556  xrltnsym  9985  xsubge0  10073  0fz1  10237  seqf  10681  seq3f1oleml  10733  exp1  10762  expp1  10763  resqrexlemf1  11514  resqrexlemfp1  11515  clim2ser  11843  clim2ser2  11844  isermulc2  11846  summodclem3  11886  fisumss  11898  fsum3cvg3  11902  iserabs  11981  isumshft  11996  isumsplit  11997  geoisum1  12025  geoisum1c  12026  cvgratnnlemnexp  12030  cvgratz  12038  mertenslem2  12042  clim2prod  12045  clim2divap  12046  fprodseq  12089  prodssdc  12095  fprodssdc  12096  effsumlt  12198  efgt1p  12202  gcd0id  12495  nninfctlemfo  12556  lcmgcd  12595  lcmdvds  12596  lcmid  12597  isprm2lem  12633  pcmpt  12861  ennnfonelemjn  12968  issgrpd  13440  mulg1  13661  srglmhm  13951  srgrmhm  13952  ringlghm  14019  ringrghm  14020  neipsm  14822  xmetpsmet  15037  comet  15167  metrest  15174  expcncf  15277  lgscllem  15680  lgsdir2  15706  lgsdirnn0  15720  lgsdinn0  15721  cvgcmp2nlemabs  16359  nconstwlpolem  16392