Theorem syl3an1 1304

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 1209	. 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 1002

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 1004

This theorem is referenced by:  syl3an1b  1307  syl3an1br  1310  wepo  4450  f1ofveu  5989  fovcdmda  6149  smoiso  6448  tfrcl  6510  omv  6601  oeiv  6602  nndi  6632  nnmsucr  6634  f1oen2g  6906  f1dom2g  6907  undiffi  7087  prarloclemarch2  7606  distrnq0  7646  ltprordil  7776  1idprl  7777  1idpru  7778  ltpopr  7782  ltexprlemopu  7790  ltexprlemdisj  7793  ltexprlemfl  7796  ltexprlemfu  7798  ltexprlemru  7799  recexprlemdisj  7817  recexprlemss1l  7822  recexprlemss1u  7823  cnegexlem1  8321  msqge0  8763  mulge0  8766  divnegap  8853  divdiv32ap  8867  divneg2ap  8883  peano2uz  9778  lbzbi  9811  negqmod0  10553  modqmuladdnn0  10590  expnlbnd  10886  fun2dmnop  11070  shftfvalg  11329  xrmaxaddlem  11771  retanclap  12233  tannegap  12239  demoivreALT  12285  gcd0id  12500  isprm3  12640  euclemma  12668  phiprmpw  12744  fermltl  12756  sgrpcl  13442  mndcl  13456  imasmnd2  13485  grpcl  13541  dfgrp2  13560  grprcan  13570  grpsubcl  13613  imasgrp2  13647  mhmid  13652  mhmmnd  13653  mulginvcom  13684  mulgnndir  13688  mulgnnass  13694  qusgrp  13769  ghmmulg  13793  ghmrn  13794  ghmeqker  13808  ablcom  13840  ablinvadd  13847  ghmcmn  13864  rngacl  13905  rngpropd  13918  srgacl  13945  srgcom  13946  ringacl  13993  imasring  14027  subrngacl  14172  subrgacl  14196  subrgugrp  14204  lmodacl  14263  lmodmcl  14264  lmodvacl  14266  lmodvsubcl  14296  lmod4  14301  lmodvaddsub4  14303  lmodvpncan  14304  lmodvnpcan  14305  lmodsubeq0  14310  psmetcl  15000  xmetcl  15026  metcl  15027  meteq0  15034  metge0  15040  metsym  15045  blelrnps  15093  blelrn  15094  blssm  15095  blres  15108  mscl  15139  xmscl  15140  xmsge0  15141  xmseq0  15142  xmssym  15143  mopnin  15161  sincosq1sgn  15500  sincosq2sgn  15501  sincosq3sgn  15502  sincosq4sgn  15503  lgsneg1  15704  usgredg2vtx  16015  uspgredg2vtxeu  16016  usgredg2vtxeu  16017