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  7699  distrnq0  7739  ltprordil  7869  1idprl  7870  1idpru  7871  ltpopr  7875  ltexprlemopu  7883  ltexprlemdisj  7886  ltexprlemfl  7889  ltexprlemfu  7891  ltexprlemru  7892  recexprlemdisj  7910  recexprlemss1l  7915  recexprlemss1u  7916  cnegexlem1  8413  msqge0  8855  mulge0  8858  divnegap  8945  divdiv32ap  8959  divneg2ap  8975  peano2uz  9878  lbzbi  9911  negqmod0  10656  modqmuladdnn0  10693  expnlbnd  10989  fun2dmnop  11178  shftfvalg  11458  xrmaxaddlem  11900  retanclap  12363  tannegap  12369  demoivreALT  12415  gcd0id  12630  isprm3  12770  euclemma  12798  phiprmpw  12874  fermltl  12886  sgrpcl  13572  mndcl  13586  imasmnd2  13615  grpcl  13671  dfgrp2  13690  grprcan  13700  grpsubcl  13743  imasgrp2  13777  mhmid  13782  mhmmnd  13783  mulginvcom  13814  mulgnndir  13818  mulgnnass  13824  qusgrp  13899  ghmmulg  13923  ghmrn  13924  ghmeqker  13938  ablcom  13970  ablinvadd  13977  ghmcmn  13994  rngacl  14036  rngpropd  14049  srgacl  14076  srgcom  14077  ringacl  14124  imasring  14158  subrngacl  14303  subrgacl  14327  subrgugrp  14335  lmodacl  14395  lmodmcl  14396  lmodvacl  14398  lmodvsubcl  14428  lmod4  14433  lmodvaddsub4  14435  lmodvpncan  14436  lmodvnpcan  14437  lmodsubeq0  14442  psmetcl  15137  xmetcl  15163  metcl  15164  meteq0  15171  metge0  15177  metsym  15182  blelrnps  15230  blelrn  15231  blssm  15232  blres  15245  mscl  15276  xmscl  15277  xmsge0  15278  xmseq0  15279  xmssym  15280  mopnin  15298  sincosq1sgn  15637  sincosq2sgn  15638  sincosq3sgn  15639  sincosq4sgn  15640  lgsneg1  15844  usgredg2vtx  16158  uspgredg2vtxeu  16159  usgredg2vtxeu  16160