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  6578  tfrcl  6640  omv  6733  oeiv  6734  nndi  6764  nnmsucr  6766  f1oen2g  7047  f1dom2g  7048  undiffi  7238  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  9998  lbzbi  10031  negqmod0  10788  modqmuladdnn0  10825  expnlbnd  11122  fun2dmnop  11324  shftfvalg  11604  xrmaxaddlem  12050  retanclap  12513  tannegap  12519  demoivreALT  12565  gcd0id  12780  isprm3  12920  euclemma  12949  phiprmpw  13028  fermltl  13040  sgrpcl  13782  mndcl  13794  imasmnd2  13817  grpcl  13871  dfgrp2  13890  grprcan  13900  grpsubcl  13943  imasgrp2  13971  mhmid  13976  mhmmnd  13977  mulginvcom  14008  mulgnndir  14012  mulgnnass  14018  qusgrp  14093  ghmmulg  14117  ghmrn  14118  ghmeqker  14132  ablcom  14195  ablinvadd  14203  ghmcmn  14220  rngacl  14347  rngpropd  14360  srgacl  14392  srgcom  14393  ringacl  14441  imasring  14477  subrngacl  14624  subrgacl  14648  subrgugrp  14656  ringen1zr0  14730  lmodacl  14743  lmodmcl  14744  lmodvacl  14746  lmodvsubcl  14777  lmod4  14782  lmodvaddsub4  14784  lmodvpncan  14785  lmodvnpcan  14786  lmodsubeq0  14791  ascldimul  15139  rnasclmulcl  15145  psmetcl  15569  xmetcl  15595  metcl  15596  meteq0  15603  metge0  15609  metsym  15614  blelrnps  15662  blelrn  15663  blssm  15664  blres  15677  mscl  15708  xmscl  15709  xmsge0  15710  xmseq0  15711  xmssym  15712  mopnin  15730  sincosq1sgn  16070  sincosq2sgn  16071  sincosq3sgn  16072  sincosq4sgn  16073  lgsneg1  16366  usgredg2vtx  16680  uspgredg2vtxeu  16681  usgredg2vtxeu  16682