Theorem syl3an1 1311

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 1216	. 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 1009

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 1011

This theorem is referenced by:  syl3an1b  1314  syl3an1br  1317  wepo  4499  f1ofveu  6063  fovcdmda  6223  suppvalfng  6470  smoiso  6563  tfrcl  6625  omv  6718  oeiv  6719  nndi  6749  nnmsucr  6751  f1oen2g  7031  f1dom2g  7032  undiffi  7222  prarloclemarch2  7776  distrnq0  7816  ltprordil  7946  1idprl  7947  1idpru  7948  ltpopr  7952  ltexprlemopu  7960  ltexprlemdisj  7963  ltexprlemfl  7966  ltexprlemfu  7968  ltexprlemru  7969  recexprlemdisj  7987  recexprlemss1l  7992  recexprlemss1u  7993  cnegexlem1  8491  msqge0  8934  mulge0  8937  divnegap  9026  divdiv32ap  9040  divneg2ap  9056  peano2uz  9962  lbzbi  9995  negqmod0  10746  modqmuladdnn0  10783  expnlbnd  11080  fun2dmnop  11281  shftfvalg  11561  xrmaxaddlem  12004  retanclap  12467  tannegap  12473  demoivreALT  12519  gcd0id  12734  isprm3  12874  euclemma  12902  phiprmpw  12978  fermltl  12990  sgrpcl  13701  mndcl  13713  imasmnd2  13736  grpcl  13790  dfgrp2  13809  grprcan  13819  grpsubcl  13862  imasgrp2  13890  mhmid  13895  mhmmnd  13896  mulginvcom  13927  mulgnndir  13931  mulgnnass  13937  qusgrp  14012  ghmmulg  14036  ghmrn  14037  ghmeqker  14051  ablcom  14083  ablinvadd  14091  ghmcmn  14108  rngacl  14216  rngpropd  14229  srgacl  14260  srgcom  14261  ringacl  14308  imasring  14342  subrngacl  14489  subrgacl  14513  subrgugrp  14521  ringen1zr0  14595  lmodacl  14608  lmodmcl  14609  lmodvacl  14611  lmodvsubcl  14641  lmod4  14646  lmodvaddsub4  14648  lmodvpncan  14649  lmodvnpcan  14650  lmodsubeq0  14655  psmetcl  15350  xmetcl  15376  metcl  15377  meteq0  15384  metge0  15390  metsym  15395  blelrnps  15443  blelrn  15444  blssm  15445  blres  15458  mscl  15489  xmscl  15490  xmsge0  15491  xmseq0  15492  xmssym  15493  mopnin  15511  sincosq1sgn  15850  sincosq2sgn  15851  sincosq3sgn  15852  sincosq4sgn  15853  lgsneg1  16058  usgredg2vtx  16372  uspgredg2vtxeu  16373  usgredg2vtxeu  16374