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  4482  f1ofveu  6040  fovcdmda  6200  suppvalfng  6442  smoiso  6535  tfrcl  6597  omv  6690  oeiv  6691  nndi  6721  nnmsucr  6723  f1oen2g  6996  f1dom2g  6997  undiffi  7187  prarloclemarch2  7736  distrnq0  7776  ltprordil  7906  1idprl  7907  1idpru  7908  ltpopr  7912  ltexprlemopu  7920  ltexprlemdisj  7923  ltexprlemfl  7926  ltexprlemfu  7928  ltexprlemru  7929  recexprlemdisj  7947  recexprlemss1l  7952  recexprlemss1u  7953  cnegexlem1  8450  msqge0  8892  mulge0  8895  divnegap  8982  divdiv32ap  8996  divneg2ap  9012  peano2uz  9918  lbzbi  9951  negqmod0  10697  modqmuladdnn0  10734  expnlbnd  11030  fun2dmnop  11227  shftfvalg  11507  xrmaxaddlem  11949  retanclap  12412  tannegap  12418  demoivreALT  12464  gcd0id  12679  isprm3  12819  euclemma  12847  phiprmpw  12923  fermltl  12935  sgrpcl  13639  mndcl  13653  imasmnd2  13682  grpcl  13738  dfgrp2  13757  grprcan  13767  grpsubcl  13810  imasgrp2  13844  mhmid  13849  mhmmnd  13850  mulginvcom  13881  mulgnndir  13885  mulgnnass  13891  qusgrp  13966  ghmmulg  13990  ghmrn  13991  ghmeqker  14005  ablcom  14037  ablinvadd  14044  ghmcmn  14061  rngacl  14103  rngpropd  14116  srgacl  14143  srgcom  14144  ringacl  14191  imasring  14225  subrngacl  14370  subrgacl  14394  subrgugrp  14402  lmodacl  14464  lmodmcl  14465  lmodvacl  14467  lmodvsubcl  14497  lmod4  14502  lmodvaddsub4  14504  lmodvpncan  14505  lmodvnpcan  14506  lmodsubeq0  14511  psmetcl  15208  xmetcl  15234  metcl  15235  meteq0  15242  metge0  15248  metsym  15253  blelrnps  15301  blelrn  15302  blssm  15303  blres  15316  mscl  15347  xmscl  15348  xmsge0  15349  xmseq0  15350  xmssym  15351  mopnin  15369  sincosq1sgn  15708  sincosq2sgn  15709  sincosq3sgn  15710  sincosq4sgn  15711  lgsneg1  15915  usgredg2vtx  16229  uspgredg2vtxeu  16230  usgredg2vtxeu  16231