Theorem syl3an1 1306

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 1211	. 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 1004

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 1006

This theorem is referenced by:  syl3an1b  1309  syl3an1br  1312  wepo  4456  f1ofveu  6006  fovcdmda  6166  smoiso  6468  tfrcl  6530  omv  6623  oeiv  6624  nndi  6654  nnmsucr  6656  f1oen2g  6928  f1dom2g  6929  undiffi  7117  prarloclemarch2  7639  distrnq0  7679  ltprordil  7809  1idprl  7810  1idpru  7811  ltpopr  7815  ltexprlemopu  7823  ltexprlemdisj  7826  ltexprlemfl  7829  ltexprlemfu  7831  ltexprlemru  7832  recexprlemdisj  7850  recexprlemss1l  7855  recexprlemss1u  7856  cnegexlem1  8354  msqge0  8796  mulge0  8799  divnegap  8886  divdiv32ap  8900  divneg2ap  8916  peano2uz  9817  lbzbi  9850  negqmod0  10594  modqmuladdnn0  10631  expnlbnd  10927  fun2dmnop  11116  shftfvalg  11396  xrmaxaddlem  11838  retanclap  12301  tannegap  12307  demoivreALT  12353  gcd0id  12568  isprm3  12708  euclemma  12736  phiprmpw  12812  fermltl  12824  sgrpcl  13510  mndcl  13524  imasmnd2  13553  grpcl  13609  dfgrp2  13628  grprcan  13638  grpsubcl  13681  imasgrp2  13715  mhmid  13720  mhmmnd  13721  mulginvcom  13752  mulgnndir  13756  mulgnnass  13762  qusgrp  13837  ghmmulg  13861  ghmrn  13862  ghmeqker  13876  ablcom  13908  ablinvadd  13915  ghmcmn  13932  rngacl  13974  rngpropd  13987  srgacl  14014  srgcom  14015  ringacl  14062  imasring  14096  subrngacl  14241  subrgacl  14265  subrgugrp  14273  lmodacl  14332  lmodmcl  14333  lmodvacl  14335  lmodvsubcl  14365  lmod4  14370  lmodvaddsub4  14372  lmodvpncan  14373  lmodvnpcan  14374  lmodsubeq0  14379  psmetcl  15069  xmetcl  15095  metcl  15096  meteq0  15103  metge0  15109  metsym  15114  blelrnps  15162  blelrn  15163  blssm  15164  blres  15177  mscl  15208  xmscl  15209  xmsge0  15210  xmseq0  15211  xmssym  15212  mopnin  15230  sincosq1sgn  15569  sincosq2sgn  15570  sincosq3sgn  15571  sincosq4sgn  15572  lgsneg1  15773  usgredg2vtx  16087  uspgredg2vtxeu  16088  usgredg2vtxeu  16089