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  4223  imainss  5059  xpexr2m  5085  funeu2  5258  imadiflem  5311  fnop  5335  ssimaex  5594  isosolem  5842  acexmidlem2  5889  fnovex  5925  cnvoprab  6254  smores3  6313  freccllem  6422  riinerm  6629  pw1fin  6933  enq0sym  7456  peano5nnnn  7916  axcaucvglemres  7923  uzind3  9391  xrltnsym  9818  xsubge0  9906  0fz1  10070  seqf  10487  seq3f1oleml  10529  exp1  10552  expp1  10553  resqrexlemf1  11044  resqrexlemfp1  11045  clim2ser  11372  clim2ser2  11373  isermulc2  11375  summodclem3  11415  fisumss  11427  fsum3cvg3  11431  iserabs  11510  isumshft  11525  isumsplit  11526  geoisum1  11554  geoisum1c  11555  cvgratnnlemnexp  11559  cvgratz  11567  mertenslem2  11571  clim2prod  11574  clim2divap  11575  fprodseq  11618  prodssdc  11624  fprodssdc  11625  effsumlt  11727  efgt1p  11731  gcd0id  12007  lcmgcd  12105  lcmdvds  12106  lcmid  12107  isprm2lem  12143  pcmpt  12370  ennnfonelemjn  12448  issgrpd  12868  mulg1  13062  srglmhm  13340  srgrmhm  13341  neipsm  14091  xmetpsmet  14306  comet  14436  metrest  14443  expcncf  14529  lgscllem  14845  lgsdir2  14871  lgsdirnn0  14885  lgsdinn0  14886  cvgcmp2nlemabs  15218  nconstwlpolem  15251