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  7787  distrnq0  7827  ltprordil  7957  1idprl  7958  1idpru  7959  ltpopr  7963  ltexprlemopu  7971  ltexprlemdisj  7974  ltexprlemfl  7977  ltexprlemfu  7979  ltexprlemru  7980  recexprlemdisj  7998  recexprlemss1l  8003  recexprlemss1u  8004  cnegexlem1  8503  msqge0  8947  mulge0  8950  divnegap  9039  divdiv32ap  9053  divneg2ap  9069  peano2uz  9993  lbzbi  10026  negqmod0  10783  modqmuladdnn0  10820  expnlbnd  11117  fun2dmnop  11319  shftfvalg  11599  xrmaxaddlem  12045  retanclap  12508  tannegap  12514  demoivreALT  12560  gcd0id  12775  isprm3  12915  euclemma  12944  phiprmpw  13023  fermltl  13035  sgrpcl  13777  mndcl  13789  imasmnd2  13812  grpcl  13866  dfgrp2  13885  grprcan  13895  grpsubcl  13938  imasgrp2  13966  mhmid  13971  mhmmnd  13972  mulginvcom  14003  mulgnndir  14007  mulgnnass  14013  qusgrp  14088  ghmmulg  14112  ghmrn  14113  ghmeqker  14127  ablcom  14190  ablinvadd  14198  ghmcmn  14215  rngacl  14325  rngpropd  14338  srgacl  14370  srgcom  14371  ringacl  14419  imasring  14453  subrngacl  14600  subrgacl  14624  subrgugrp  14632  ringen1zr0  14706  lmodacl  14719  lmodmcl  14720  lmodvacl  14722  lmodvsubcl  14753  lmod4  14758  lmodvaddsub4  14760  lmodvpncan  14761  lmodvnpcan  14762  lmodsubeq0  14767  ascldimul  15115  rnasclmulcl  15121  psmetcl  15518  xmetcl  15544  metcl  15545  meteq0  15552  metge0  15558  metsym  15563  blelrnps  15611  blelrn  15612  blssm  15613  blres  15626  mscl  15657  xmscl  15658  xmsge0  15659  xmseq0  15660  xmssym  15661  mopnin  15679  sincosq1sgn  16019  sincosq2sgn  16020  sincosq3sgn  16021  sincosq4sgn  16022  lgsneg1  16310  usgredg2vtx  16624  uspgredg2vtxeu  16625  usgredg2vtxeu  16626