Theorem syl3an1 1307

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 1212	. 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 1005

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  df-3an 1007

This theorem is referenced by:  syl3an1b  1310  syl3an1br  1313  wepo  4462  f1ofveu  6016  fovcdmda  6176  suppvalfng  6418  smoiso  6511  tfrcl  6573  omv  6666  oeiv  6667  nndi  6697  nnmsucr  6699  f1oen2g  6971  f1dom2g  6972  undiffi  7160  prarloclemarch2  7682  distrnq0  7722  ltprordil  7852  1idprl  7853  1idpru  7854  ltpopr  7858  ltexprlemopu  7866  ltexprlemdisj  7869  ltexprlemfl  7872  ltexprlemfu  7874  ltexprlemru  7875  recexprlemdisj  7893  recexprlemss1l  7898  recexprlemss1u  7899  cnegexlem1  8397  msqge0  8839  mulge0  8842  divnegap  8929  divdiv32ap  8943  divneg2ap  8959  peano2uz  9860  lbzbi  9893  negqmod0  10637  modqmuladdnn0  10674  expnlbnd  10970  fun2dmnop  11159  shftfvalg  11439  xrmaxaddlem  11881  retanclap  12344  tannegap  12350  demoivreALT  12396  gcd0id  12611  isprm3  12751  euclemma  12779  phiprmpw  12855  fermltl  12867  sgrpcl  13553  mndcl  13567  imasmnd2  13596  grpcl  13652  dfgrp2  13671  grprcan  13681  grpsubcl  13724  imasgrp2  13758  mhmid  13763  mhmmnd  13764  mulginvcom  13795  mulgnndir  13799  mulgnnass  13805  qusgrp  13880  ghmmulg  13904  ghmrn  13905  ghmeqker  13919  ablcom  13951  ablinvadd  13958  ghmcmn  13975  rngacl  14017  rngpropd  14030  srgacl  14057  srgcom  14058  ringacl  14105  imasring  14139  subrngacl  14284  subrgacl  14308  subrgugrp  14316  lmodacl  14375  lmodmcl  14376  lmodvacl  14378  lmodvsubcl  14408  lmod4  14413  lmodvaddsub4  14415  lmodvpncan  14416  lmodvnpcan  14417  lmodsubeq0  14422  psmetcl  15117  xmetcl  15143  metcl  15144  meteq0  15151  metge0  15157  metsym  15162  blelrnps  15210  blelrn  15211  blssm  15212  blres  15225  mscl  15256  xmscl  15257  xmsge0  15258  xmseq0  15259  xmssym  15260  mopnin  15278  sincosq1sgn  15617  sincosq2sgn  15618  sincosq3sgn  15619  sincosq4sgn  15620  lgsneg1  15821  usgredg2vtx  16135  uspgredg2vtxeu  16136  usgredg2vtxeu  16137