Theorem syl3an1 1266

Description: A syllogism inference. (Contributed by NM, 22-Aug-1995.)

Hypotheses

Ref	Expression
syl3an1.1	|- ( ph -> ps )
syl3an1.2	|- ( ( ps /\ ch /\ th ) -> ta )

Assertion

Ref	Expression
syl3an1	|- ( ( ph /\ ch /\ th ) -> ta )

Proof of Theorem syl3an1

Step	Hyp	Ref	Expression
1		syl3an1.1	. . 3 |- ( ph -> ps )
2	1	3anim1i 1180	. 2 |- ( ( ph /\ ch /\ th ) -> ( ps /\ ch /\ th ) )
3		syl3an1.2	. 2 |- ( ( ps /\ ch /\ th ) -> ta )
4	2, 3	syl 14	1 |- ( ( ph /\ ch /\ th ) -> ta )

Syntax hints:   -> wi 4   /\ w3a 973

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

This theorem depends on definitions:  df-bi 116  df-3an 975

This theorem is referenced by:  syl3an1b  1269  syl3an1br  1272  wepo  4344  f1ofveu  5841  fovrnda  5996  smoiso  6281  tfrcl  6343  omv  6434  oeiv  6435  nndi  6465  nnmsucr  6467  f1oen2g  6733  f1dom2g  6734  undiffi  6902  prarloclemarch2  7381  distrnq0  7421  ltprordil  7551  1idprl  7552  1idpru  7553  ltpopr  7557  ltexprlemopu  7565  ltexprlemdisj  7568  ltexprlemfl  7571  ltexprlemfu  7573  ltexprlemru  7574  recexprlemdisj  7592  recexprlemss1l  7597  recexprlemss1u  7598  cnegexlem1  8094  msqge0  8535  mulge0  8538  divnegap  8623  divdiv32ap  8637  divneg2ap  8653  peano2uz  9542  lbzbi  9575  negqmod0  10287  modqmuladdnn0  10324  expnlbnd  10600  shftfvalg  10782  xrmaxaddlem  11223  retanclap  11685  tannegap  11691  demoivreALT  11736  gcd0id  11934  isprm3  12072  euclemma  12100  phiprmpw  12176  fermltl  12188  mndcl  12659  grpcl  12716  dfgrp2  12732  grprcan  12740  psmetcl  13120  xmetcl  13146  metcl  13147  meteq0  13154  metge0  13160  metsym  13165  blelrnps  13213  blelrn  13214  blssm  13215  blres  13228  mscl  13259  xmscl  13260  xmsge0  13261  xmseq0  13262  xmssym  13263  mopnin  13281  sincosq1sgn  13541  sincosq2sgn  13542  sincosq3sgn  13543  sincosq4sgn  13544  lgsneg1  13720