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  8502  msqge0  8946  mulge0  8949  divnegap  9038  divdiv32ap  9052  divneg2ap  9068  peano2uz  9992  lbzbi  10025  negqmod0  10781  modqmuladdnn0  10818  expnlbnd  11115  fun2dmnop  11317  shftfvalg  11597  xrmaxaddlem  12042  retanclap  12505  tannegap  12511  demoivreALT  12557  gcd0id  12772  isprm3  12912  euclemma  12941  phiprmpw  13020  fermltl  13032  sgrpcl  13773  mndcl  13785  imasmnd2  13808  grpcl  13862  dfgrp2  13881  grprcan  13891  grpsubcl  13934  imasgrp2  13962  mhmid  13967  mhmmnd  13968  mulginvcom  13999  mulgnndir  14003  mulgnnass  14009  qusgrp  14084  ghmmulg  14108  ghmrn  14109  ghmeqker  14123  ablcom  14155  ablinvadd  14163  ghmcmn  14180  rngacl  14290  rngpropd  14303  srgacl  14335  srgcom  14336  ringacl  14384  imasring  14418  subrngacl  14565  subrgacl  14589  subrgugrp  14597  ringen1zr0  14671  lmodacl  14684  lmodmcl  14685  lmodvacl  14687  lmodvsubcl  14718  lmod4  14723  lmodvaddsub4  14725  lmodvpncan  14726  lmodvnpcan  14727  lmodsubeq0  14732  ascldimul  15080  rnasclmulcl  15086  psmetcl  15476  xmetcl  15502  metcl  15503  meteq0  15510  metge0  15516  metsym  15521  blelrnps  15569  blelrn  15570  blssm  15571  blres  15584  mscl  15615  xmscl  15616  xmsge0  15617  xmseq0  15618  xmssym  15619  mopnin  15637  sincosq1sgn  15977  sincosq2sgn  15978  sincosq3sgn  15979  sincosq4sgn  15980  lgsneg1  16242  usgredg2vtx  16556  uspgredg2vtxeu  16557  usgredg2vtxeu  16558