Theorem syl3an3 1361

Description: A syllogism inference. (Contributed by NM, 22-Aug-1995.)

Hypotheses

Ref	Expression
syl3an3.1	|- ( ph -> th )
syl3an3.2	|- ( ( ps /\ ch /\ th ) -> ta )

Assertion

Ref	Expression
syl3an3	|- ( ( ps /\ ch /\ ph ) -> ta )

Proof of Theorem syl3an3

Step	Hyp	Ref	Expression
1		syl3an3.1	. . 3 |- ( ph -> th )
2		syl3an3.2	. . . 4 |- ( ( ps /\ ch /\ th ) -> ta )
3	2	3exp 1264	. . 3 |- ( ps -> ( ch -> ( th -> ta ) ) )
4	1, 3	syl7 74	. 2 |- ( ps -> ( ch -> ( ph -> ta ) ) )
5	4	3imp 1256	1 |- ( ( ps /\ ch /\ ph ) -> ta )

Syntax hints:   -> wi 4   /\ w3a 1037

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386  df-3an 1039

This theorem is referenced by:  syl3an3b  1364  syl3an3br  1367  vtoclgftOLD  3255  disji  4637  ovmpt2x  6789  ovmpt2ga  6790  wfrlem14  7428  unbnn2  8217  axdc3lem4  9275  axdclem2  9342  gruiin  9632  gruen  9634  divass  10703  ltmul2  10874  xleadd1  12085  xltadd2  12087  xlemul1  12120  xltmul2  12123  elfzo  12472  modcyc2  12706  faclbnd5  13085  relexprel  13779  subcn2  14325  mulcn2  14326  ndvdsp1  15135  gcddiv  15268  lcmneg  15316  lubel  17122  gsumccatsn  17380  mulgaddcom  17564  oddvdsi  17967  odcong  17968  odeq  17969  efgsp1  18150  lspsnss  18990  lindsmm2  20168  mulmarep1el  20378  mdetunilem4  20421  iuncld  20849  neips  20917  opnneip  20923  comppfsc  21335  hmeof1o2  21566  ordthmeo  21605  ufinffr  21733  elfm3  21754  utop3cls  22055  blcntrps  22217  blcntr  22218  neibl  22306  blnei  22307  metss  22313  stdbdmetval  22319  prdsms  22336  blval2  22367  lmmbr  23056  lmmbr2  23057  iscau2  23075  bcthlem1  23121  bcthlem3  23123  bcthlem4  23124  dvn2bss  23693  dvfsumrlim  23794  dvfsumrlim2  23795  cxpexpz  24413  cxpsub  24428  relogbzexp  24514  upgr4cycl4dv4e  27045  konigsbergssiedgwpr  27110  hvaddsub12  27895  hvaddsubass  27898  hvsubdistr1  27906  hvsubcan  27931  hhssnv  28121  spanunsni  28438  homco1  28660  homulass  28661  hoadddir  28663  hosubdi  28667  hoaddsubass  28674  hosubsub4  28677  lnopmi  28859  adjlnop  28945  mdsymlem5  29266  disjif  29391  disjif2  29394  ind0  30080  sigaclfu  30182  bnj544  30964  bnj561  30973  bnj562  30974  bnj594  30982  clsint2  32324  ftc1anclem6  33490  isbnd2  33582  blbnd  33586  isdrngo2  33757  atnem0  34605  hlrelat5N  34687  ltrnel  35425  ltrnat  35426  ltrncnvat  35427  jm2.22  37562  jm2.23  37563  dvconstbi  38533  eelT11  38932  eelT12  38934  eelTT1  38935  eelT01  38936  eel0T1  38937  liminfvalxr  40015  rmfsupp  42155  mndpfsupp  42157  scmfsupp  42159  dignn0flhalflem2  42410