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 )

This proof depends on syntax axioms:   -> wi 4   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  syl3an1b  1314  syl3an1br  1317  wepo  4506  f1ofveu  6076  fovcdmda  6236  suppvalfng  6484  smoiso  6577  tfrcl  6639  omv  6732  oeiv  6733  nndi  6763  nnmsucr  6765  f1oen2g  7045  f1dom2g  7046  undiffi  7236  prarloclemarch2  7792  distrnq0  7832  ltprordil  7962  1idprl  7963  1idpru  7964  ltpopr  7968  ltexprlemopu  7976  ltexprlemdisj  7979  ltexprlemfl  7982  ltexprlemfu  7984  ltexprlemru  7985  recexprlemdisj  8003  recexprlemss1l  8008  recexprlemss1u  8009  cnegexlem1  8508  msqge0  8952  mulge0  8955  divnegap  9044  divdiv32ap  9058  divneg2ap  9074  peano2uz  9999  lbzbi  10032  negqmod0  10789  modqmuladdnn0  10826  expnlbnd  11123  fun2dmnop  11325  shftfvalg  11605  xrmaxaddlem  12051  retanclap  12514  tannegap  12520  demoivreALT  12566  gcd0id  12781  isprm3  12921  euclemma  12950  phiprmpw  13029  fermltl  13041  sgrpcl  13783  mndcl  13795  imasmnd2  13818  grpcl  13872  dfgrp2  13891  grprcan  13901  grpsubcl  13944  imasgrp2  13972  mhmid  13977  mhmmnd  13978  mulginvcom  14009  mulgnndir  14013  mulgnnass  14019  qusgrp  14094  ghmmulg  14118  ghmrn  14119  ghmeqker  14133  ablcom  14196  ablinvadd  14204  ghmcmn  14221  rngacl  14348  rngpropd  14361  srgacl  14393  srgcom  14394  ringacl  14442  imasring  14478  subrngacl  14625  subrgacl  14649  subrgugrp  14657  ringen1zr0  14731  lmodacl  14744  lmodmcl  14745  lmodvacl  14747  lmodvsubcl  14778  lmod4  14783  lmodvaddsub4  14785  lmodvpncan  14786  lmodvnpcan  14787  lmodsubeq0  14792  ascldimul  15140  rnasclmulcl  15146  psmetcl  15552  xmetcl  15578  metcl  15579  meteq0  15586  metge0  15592  metsym  15597  blelrnps  15645  blelrn  15646  blssm  15647  blres  15660  mscl  15691  xmscl  15692  xmsge0  15693  xmseq0  15694  xmssym  15695  mopnin  15713  sincosq1sgn  16053  sincosq2sgn  16054  sincosq3sgn  16055  sincosq4sgn  16056  lgsneg1  16349  usgredg2vtx  16663  uspgredg2vtxeu  16664  usgredg2vtxeu  16665