Theorem syl3an2 1261

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

Hypotheses

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

Assertion

Ref	Expression
syl3an2	|- ( ( ps /\ ph /\ th ) -> ta )

Proof of Theorem syl3an2

Step	Hyp	Ref	Expression
1		syl3an2.1	. . 3 |- ( ph -> ch )
2		syl3an2.2	. . . 4 |- ( ( ps /\ ch /\ th ) -> ta )
3	2	3exp 1194	. . 3 |- ( ps -> ( ch -> ( th -> ta ) ) )
4	1, 3	syl5 32	. 2 |- ( ps -> ( ph -> ( th -> ta ) ) )
5	4	3imp 1189	1 |- ( ( ps /\ ph /\ th ) -> ta )

Syntax hints:   -> wi 4   /\ w3a 972

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 185  df-an 371  df-3an 974

This theorem is referenced by:  syl3an2b  1264  syl3an2br  1267  syl3anl2  1276  odi  7227  omass  7228  nndi  7271  nnmass  7272  omabslem  7294  winainf  9072  divsubdir  10243  divdiv32  10255  ltdiv2  10433  peano2uz  11140  irrmul  11213  supxrunb1  11517  fzoshftral  11899  ltdifltdiv  11942  axdc4uzlem  12068  expdiv  12192  bcval5  12372  ccats1val1  12606  rediv  12940  imdiv  12947  absdiflt  13126  absdifle  13127  iseraltlem3  13482  retancl  13751  tanneg  13757  prmdvdsexpb  14130  pmtrfb  16361  lspssp  17505  mdetunilem7  18990  m2detleiblem3  19001  m2detleiblem4  19002  pmatcollpw  19152  pmatcollpwscmat  19162  chpmatply1  19203  chfacfscmulgsum  19231  chfacfpmmulcl  19232  chfacfpmmul0  19233  chfacfpmmulgsum  19235  chfacfpmmulgsum2  19236  cayhamlem1  19237  cpmadurid  19238  cpmadugsumlemC  19246  cpmadugsumlemF  19247  cpmadugsumfi  19248  cpmidgsum2  19250  islp2  19516  fmfg  20320  fmufil  20330  flffbas  20366  lmflf  20376  uffcfflf  20410  blres  20804  caucfil  21592  cmetcusp1OLD  21661  cmetcusp1  21662  deg1mul3  22386  quotval  22557  cusgra3vnbpr  24334  gxid  25144  nvsge0  25435  hvsubass  25830  hvsubdistr2  25836  hvsubcan  25860  his2sub  25878  chlub  26296  spanunsni  26366  homco1  26589  homulass  26590  cnlnadjlem2  26856  adjmul  26880  chirredlem2  27179  atmd2  27188  mdsymlem5  27195  climuzcnv  28907  f1ocan2fv  30190  isdrngo2  30333  eluzrabdioph  30711  iocmbl  31153  lcmgcdeq  31189  dvconstbi  31212  sinhpcosh  32864  reseccl  32877  recsccl  32878  recotcl  32879  onetansqsecsq  32885  eelT11  33224  eelT12  33228  eelTT1  33230  eel0T1  33232  atncvrN  34763  cvlatcvr1  34789  rp-isfinite6  37430