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  1413  exmid1stab  4252  imainss  5098  xpexr2m  5124  funeu2  5297  imadiflem  5353  fnop  5379  ssimaex  5640  isosolem  5893  acexmidlem2  5941  fnovex  5977  cnvoprab  6320  smores3  6379  freccllem  6488  riinerm  6695  pw1fin  7007  enq0sym  7545  peano5nnnn  8005  axcaucvglemres  8012  uzind3  9486  xrltnsym  9915  xsubge0  10003  0fz1  10167  seqf  10609  seq3f1oleml  10661  exp1  10690  expp1  10691  resqrexlemf1  11319  resqrexlemfp1  11320  clim2ser  11648  clim2ser2  11649  isermulc2  11651  summodclem3  11691  fisumss  11703  fsum3cvg3  11707  iserabs  11786  isumshft  11801  isumsplit  11802  geoisum1  11830  geoisum1c  11831  cvgratnnlemnexp  11835  cvgratz  11843  mertenslem2  11847  clim2prod  11850  clim2divap  11851  fprodseq  11894  prodssdc  11900  fprodssdc  11901  effsumlt  12003  efgt1p  12007  gcd0id  12300  nninfctlemfo  12361  lcmgcd  12400  lcmdvds  12401  lcmid  12402  isprm2lem  12438  pcmpt  12666  ennnfonelemjn  12773  issgrpd  13244  mulg1  13465  srglmhm  13755  srgrmhm  13756  ringlghm  13823  ringrghm  13824  neipsm  14626  xmetpsmet  14841  comet  14971  metrest  14978  expcncf  15081  lgscllem  15484  lgsdir2  15510  lgsdirnn0  15524  lgsdinn0  15525  cvgcmp2nlemabs  15971  nconstwlpolem  16004