Theorem syl3an1 1283

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 1188	. 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 981

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 983

This theorem is referenced by:  syl3an1b  1286  syl3an1br  1289  wepo  4407  f1ofveu  5934  fovcdmda  6092  smoiso  6390  tfrcl  6452  omv  6543  oeiv  6544  nndi  6574  nnmsucr  6576  f1oen2g  6848  f1dom2g  6849  undiffi  7024  prarloclemarch2  7534  distrnq0  7574  ltprordil  7704  1idprl  7705  1idpru  7706  ltpopr  7710  ltexprlemopu  7718  ltexprlemdisj  7721  ltexprlemfl  7724  ltexprlemfu  7726  ltexprlemru  7727  recexprlemdisj  7745  recexprlemss1l  7750  recexprlemss1u  7751  cnegexlem1  8249  msqge0  8691  mulge0  8694  divnegap  8781  divdiv32ap  8795  divneg2ap  8811  peano2uz  9706  lbzbi  9739  negqmod0  10478  modqmuladdnn0  10515  expnlbnd  10811  fun2dmnop  10995  shftfvalg  11162  xrmaxaddlem  11604  retanclap  12066  tannegap  12072  demoivreALT  12118  gcd0id  12333  isprm3  12473  euclemma  12501  phiprmpw  12577  fermltl  12589  sgrpcl  13274  mndcl  13288  imasmnd2  13317  grpcl  13373  dfgrp2  13392  grprcan  13402  grpsubcl  13445  imasgrp2  13479  mhmid  13484  mhmmnd  13485  mulginvcom  13516  mulgnndir  13520  mulgnnass  13526  qusgrp  13601  ghmmulg  13625  ghmrn  13626  ghmeqker  13640  ablcom  13672  ablinvadd  13679  ghmcmn  13696  rngacl  13737  rngpropd  13750  srgacl  13777  srgcom  13778  ringacl  13825  imasring  13859  subrngacl  14003  subrgacl  14027  subrgugrp  14035  lmodacl  14094  lmodmcl  14095  lmodvacl  14097  lmodvsubcl  14127  lmod4  14132  lmodvaddsub4  14134  lmodvpncan  14135  lmodvnpcan  14136  lmodsubeq0  14141  psmetcl  14831  xmetcl  14857  metcl  14858  meteq0  14865  metge0  14871  metsym  14876  blelrnps  14924  blelrn  14925  blssm  14926  blres  14939  mscl  14970  xmscl  14971  xmsge0  14972  xmseq0  14973  xmssym  14974  mopnin  14992  sincosq1sgn  15331  sincosq2sgn  15332  sincosq3sgn  15333  sincosq4sgn  15334  lgsneg1  15535