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  4485  f1ofveu  6046  fovcdmda  6206  suppvalfng  6453  smoiso  6546  tfrcl  6608  omv  6701  oeiv  6702  nndi  6732  nnmsucr  6734  f1oen2g  7007  f1dom2g  7008  undiffi  7198  prarloclemarch2  7750  distrnq0  7790  ltprordil  7920  1idprl  7921  1idpru  7922  ltpopr  7926  ltexprlemopu  7934  ltexprlemdisj  7937  ltexprlemfl  7940  ltexprlemfu  7942  ltexprlemru  7943  recexprlemdisj  7961  recexprlemss1l  7966  recexprlemss1u  7967  cnegexlem1  8464  msqge0  8907  mulge0  8910  divnegap  8997  divdiv32ap  9011  divneg2ap  9027  peano2uz  9933  lbzbi  9966  negqmod0  10717  modqmuladdnn0  10754  expnlbnd  11051  fun2dmnop  11248  shftfvalg  11528  xrmaxaddlem  11970  retanclap  12433  tannegap  12439  demoivreALT  12485  gcd0id  12700  isprm3  12840  euclemma  12868  phiprmpw  12944  fermltl  12956  sgrpcl  13672  mndcl  13684  imasmnd2  13707  grpcl  13763  dfgrp2  13782  grprcan  13792  grpsubcl  13835  imasgrp2  13863  mhmid  13868  mhmmnd  13869  mulginvcom  13900  mulgnndir  13904  mulgnnass  13910  qusgrp  13985  ghmmulg  14009  ghmrn  14010  ghmeqker  14024  ablcom  14056  ablinvadd  14063  ghmcmn  14080  rngacl  14181  rngpropd  14194  srgacl  14225  srgcom  14226  ringacl  14273  imasring  14307  subrngacl  14454  subrgacl  14478  subrgugrp  14486  ringen1zr0  14560  lmodacl  14573  lmodmcl  14574  lmodvacl  14576  lmodvsubcl  14606  lmod4  14611  lmodvaddsub4  14613  lmodvpncan  14614  lmodvnpcan  14615  lmodsubeq0  14620  psmetcl  15317  xmetcl  15343  metcl  15344  meteq0  15351  metge0  15357  metsym  15362  blelrnps  15410  blelrn  15411  blssm  15412  blres  15425  mscl  15456  xmscl  15457  xmsge0  15458  xmseq0  15459  xmssym  15460  mopnin  15478  sincosq1sgn  15817  sincosq2sgn  15818  sincosq3sgn  15819  sincosq4sgn  15820  lgsneg1  16024  usgredg2vtx  16338  uspgredg2vtxeu  16339  usgredg2vtxeu  16340