Theorem syl3an1 1282

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 1187	. 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 980

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 982

This theorem is referenced by:  syl3an1b  1285  syl3an1br  1288  wepo  4394  f1ofveu  5910  fovcdmda  6067  smoiso  6360  tfrcl  6422  omv  6513  oeiv  6514  nndi  6544  nnmsucr  6546  f1oen2g  6814  f1dom2g  6815  undiffi  6986  prarloclemarch2  7486  distrnq0  7526  ltprordil  7656  1idprl  7657  1idpru  7658  ltpopr  7662  ltexprlemopu  7670  ltexprlemdisj  7673  ltexprlemfl  7676  ltexprlemfu  7678  ltexprlemru  7679  recexprlemdisj  7697  recexprlemss1l  7702  recexprlemss1u  7703  cnegexlem1  8201  msqge0  8643  mulge0  8646  divnegap  8733  divdiv32ap  8747  divneg2ap  8763  peano2uz  9657  lbzbi  9690  negqmod0  10423  modqmuladdnn0  10460  expnlbnd  10756  shftfvalg  10983  xrmaxaddlem  11425  retanclap  11887  tannegap  11893  demoivreALT  11939  gcd0id  12146  isprm3  12286  euclemma  12314  phiprmpw  12390  fermltl  12402  sgrpcl  13052  mndcl  13064  grpcl  13140  dfgrp2  13159  grprcan  13169  grpsubcl  13212  imasgrp2  13240  mhmid  13245  mhmmnd  13246  mulginvcom  13277  mulgnndir  13281  mulgnnass  13287  qusgrp  13362  ghmmulg  13386  ghmrn  13387  ghmeqker  13401  ablcom  13433  ablinvadd  13440  ghmcmn  13457  rngacl  13498  rngpropd  13511  srgacl  13538  srgcom  13539  ringacl  13586  imasring  13620  subrngacl  13764  subrgacl  13788  subrgugrp  13796  lmodacl  13855  lmodmcl  13856  lmodvacl  13858  lmodvsubcl  13888  lmod4  13893  lmodvaddsub4  13895  lmodvpncan  13896  lmodvnpcan  13897  lmodsubeq0  13902  psmetcl  14562  xmetcl  14588  metcl  14589  meteq0  14596  metge0  14602  metsym  14607  blelrnps  14655  blelrn  14656  blssm  14657  blres  14670  mscl  14701  xmscl  14702  xmsge0  14703  xmseq0  14704  xmssym  14705  mopnin  14723  sincosq1sgn  15062  sincosq2sgn  15063  sincosq3sgn  15064  sincosq4sgn  15065  lgsneg1  15266