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  1412  exmid1stab  4251  imainss  5097  xpexr2m  5123  funeu2  5296  imadiflem  5352  fnop  5378  ssimaex  5639  isosolem  5892  acexmidlem2  5940  fnovex  5976  cnvoprab  6319  smores3  6378  freccllem  6487  riinerm  6694  pw1fin  7006  enq0sym  7544  peano5nnnn  8004  axcaucvglemres  8011  uzind3  9485  xrltnsym  9914  xsubge0  10002  0fz1  10166  seqf  10607  seq3f1oleml  10659  exp1  10688  expp1  10689  resqrexlemf1  11290  resqrexlemfp1  11291  clim2ser  11619  clim2ser2  11620  isermulc2  11622  summodclem3  11662  fisumss  11674  fsum3cvg3  11678  iserabs  11757  isumshft  11772  isumsplit  11773  geoisum1  11801  geoisum1c  11802  cvgratnnlemnexp  11806  cvgratz  11814  mertenslem2  11818  clim2prod  11821  clim2divap  11822  fprodseq  11865  prodssdc  11871  fprodssdc  11872  effsumlt  11974  efgt1p  11978  gcd0id  12271  nninfctlemfo  12332  lcmgcd  12371  lcmdvds  12372  lcmid  12373  isprm2lem  12409  pcmpt  12637  ennnfonelemjn  12744  issgrpd  13215  mulg1  13436  srglmhm  13726  srgrmhm  13727  ringlghm  13794  ringrghm  13795  neipsm  14597  xmetpsmet  14812  comet  14942  metrest  14949  expcncf  15052  lgscllem  15455  lgsdir2  15481  lgsdirnn0  15495  lgsdinn0  15496  cvgcmp2nlemabs  15933  nconstwlpolem  15966