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  4504  f1ofveu  6073  fovcdmda  6233  suppvalfng  6480  smoiso  6573  tfrcl  6635  omv  6728  oeiv  6729  nndi  6759  nnmsucr  6761  f1oen2g  7041  f1dom2g  7042  undiffi  7232  prarloclemarch2  7786  distrnq0  7826  ltprordil  7956  1idprl  7957  1idpru  7958  ltpopr  7962  ltexprlemopu  7970  ltexprlemdisj  7973  ltexprlemfl  7976  ltexprlemfu  7978  ltexprlemru  7979  recexprlemdisj  7997  recexprlemss1l  8002  recexprlemss1u  8003  cnegexlem1  8501  msqge0  8944  mulge0  8947  divnegap  9036  divdiv32ap  9050  divneg2ap  9066  peano2uz  9983  lbzbi  10016  negqmod0  10768  modqmuladdnn0  10805  expnlbnd  11102  fun2dmnop  11303  shftfvalg  11583  xrmaxaddlem  12026  retanclap  12489  tannegap  12495  demoivreALT  12541  gcd0id  12756  isprm3  12896  euclemma  12924  phiprmpw  13000  fermltl  13012  sgrpcl  13724  mndcl  13736  imasmnd2  13759  grpcl  13813  dfgrp2  13832  grprcan  13842  grpsubcl  13885  imasgrp2  13913  mhmid  13918  mhmmnd  13919  mulginvcom  13950  mulgnndir  13954  mulgnnass  13960  qusgrp  14035  ghmmulg  14059  ghmrn  14060  ghmeqker  14074  ablcom  14106  ablinvadd  14114  ghmcmn  14131  rngacl  14241  rngpropd  14254  srgacl  14286  srgcom  14287  ringacl  14335  imasring  14369  subrngacl  14516  subrgacl  14540  subrgugrp  14548  ringen1zr0  14622  lmodacl  14635  lmodmcl  14636  lmodvacl  14638  lmodvsubcl  14669  lmod4  14674  lmodvaddsub4  14676  lmodvpncan  14677  lmodvnpcan  14678  lmodsubeq0  14683  ascldimul  15031  rnasclmulcl  15037  psmetcl  15427  xmetcl  15453  metcl  15454  meteq0  15461  metge0  15467  metsym  15472  blelrnps  15520  blelrn  15521  blssm  15522  blres  15535  mscl  15566  xmscl  15567  xmsge0  15568  xmseq0  15569  xmssym  15570  mopnin  15588  sincosq1sgn  15927  sincosq2sgn  15928  sincosq3sgn  15929  sincosq4sgn  15930  lgsneg1  16144  usgredg2vtx  16458  uspgredg2vtxeu  16459  usgredg2vtxeu  16460