Theorem syl3an1 1359

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 1248	. 2 |- ( ( ph /\ ch /\ th ) -> ( ps /\ ch /\ th ) )
3		syl3an1.2	. 2 |- ( ( ps /\ ch /\ th ) -> ta )
4	2, 3	syl 17	1 |- ( ( ph /\ ch /\ th ) -> 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:  syl3an1b  1362  syl3an1br  1365  wefrc  5108  tz7.5  5744  f1ofveu  6645  fovrnda  6805  smoiso  7459  odi  7659  nndi  7703  nnmsucr  7705  f1oen2g  7972  f1dom2g  7973  domssex2  8120  ordunifi  8210  wemappo  8454  wemapso  8456  ackbij1lem16  9057  divneg  10719  divdiv32  10733  divneg2  10749  ltdiv2  10909  fimaxre  10968  suprzcl  11457  peano2uz  11741  infssuzle  11771  lbzbi  11776  zbtwnre  11786  irrmul  11813  supxrunb1  12149  expnlbnd  12994  hash1to3  13273  fun2dmnop  13277  brfi1uzind  13280  brfi1uzindOLD  13286  brcnvtrclfvcnv  13746  retancl  14872  tanneg  14878  demoivreALT  14931  dvdscmulr  15010  dvdsmulcr  15011  gcd0id  15240  euclemma  15425  phiprmpw  15481  fermltl  15489  vdwapun  15678  vdwapid1  15679  cshwshashlem1  15802  fsets  15891  pospo  16973  latasymb  17054  mndcl  17301  imasmnd2  17327  grpcl  17430  dfgrp2  17447  grprcan  17455  grpsubcl  17495  imasgrp2  17530  mhmid  17536  mhmmnd  17537  mulginvcom  17565  qusgrp  17649  ghmmulg  17672  ghmrn  17673  ghmeqker  17687  gsumccatsymgsn  17846  ablcom  18210  ablinvadd  18215  mulgmhm  18233  mulgghm  18234  ghmcmn  18237  odadd1  18251  odadd2  18252  srgcl  18512  srgacl  18524  srgcom  18525  ringcl  18561  crngcom  18562  ringacl  18578  imasring  18619  irredlmul  18708  rhmmul  18727  drngmcl  18760  isdrngd  18772  subrgacl  18791  subrgugrp  18799  srngadd  18857  srngmul  18858  idsrngd  18862  lmodacl  18874  lmodmcl  18875  lmodvacl  18877  lmodvsubcl  18908  lmod4  18913  lmodvaddsub4  18915  lmodvpncan  18916  lmodvnpcan  18917  lmodsubeq0  18922  pwssplit3  19061  islbs2  19154  islbs3  19155  lbsext  19163  rspssp  19226  mplbas2  19470  coe1add  19634  coe1subfv  19636  coe1mul2  19639  zlmlmod  19871  psgnco  19929  ipdir  19984  ip2eq  19998  ocvin  20018  frlmsplit2  20112  ringvcl  20204  cramer  20497  chpmat1d  20641  filin  21658  filfinnfr  21681  filuni  21689  ufprim  21713  uffinfix  21731  hausflf  21801  uffcfflf  21843  cnextcn  21871  tmdmulg  21896  tsmsxplem1  21956  psmetcl  22112  xmetcl  22136  metcl  22137  meteq0  22144  metge0  22150  metsym  22155  metgt0  22164  blelrnps  22221  blelrn  22222  blssm  22223  blres  22236  mscl  22266  xmscl  22267  xmsge0  22268  xmseq0  22269  xmssym  22270  mopnin  22302  nmf2  22397  ngpdsr  22409  ngpds2  22410  ngpds2r  22411  ngpds3  22412  ngpds3r  22413  nmge0  22421  nmeq0  22422  nm2dif  22429  nmmul  22468  nlmmul0or  22487  nmods  22548  clmsub  22880  clmacl  22884  clmmcl  22885  clmsubcl  22886  clmvscl  22888  clmvsubval  22909  ncvsprp  22952  ncvsdif  22955  ncvspds  22961  cphnmvs  22990  cphipcl  22991  cphipcj  22999  cphorthcom  23001  cphipval2  23040  4cphipval2  23041  cphipval  23042  fmcfil  23070  mbfi1fseqlem3  23484  mbfi1fseqlem4  23485  mbfi1fseqlem5  23486  deg1ldgdomn  23854  drnguc1p  23930  quotval  24047  sincosq1sgn  24250  sincosq2sgn  24251  sincosq3sgn  24252  sincosq4sgn  24253  efabl  24296  lgsneg1  25047  dchrisumlem3  25180  ax5seglem2  25809  usgredg2vtx  26111  uspgredg2vtxeu  26112  usgredg2vtxeu  26113  cplgr3v  26331  vtxdumgr0nedg  26389  wlkwwlkinj  26782  wlkwwlksur  26783  clwlkclwwlk  26903  clwlksfclwwlk  26962  frgrncvvdeqlem8  27170  frgr2wsp1  27194  grpocl  27354  grpodivcl  27393  ablomuldiv  27406  ablodivdiv4  27408  ablonnncan  27410  ablonnncan1  27412  vccl  27418  nvgcl  27475  nvcom  27476  nvadd4  27480  nvscl  27481  nvmval  27497  nvmcl  27501  nmcvcn  27550  nmlnoubi  27651  isblo3i  27656  blometi  27658  dipsubdir  27703  hlpar2  27752  hlpar  27753  hlcom  27756  hlipcj  27767  hlipgt0  27770  his52  27944  shintcli  28188  chlub  28368  homulass  28661  adjadj  28795  nmophmi  28890  kbass6  28980  atcvatlem  29244  mdsymlem3  29264  mdsymlem5  29266  rexdiv  29634  tltnle  29662  tlt3  29665  toslublem  29667  tosglblem  29669  archiabllem1b  29746  archiabllem2  29751  slmdacl  29762  slmdmcl  29763  slmdvacl  29765  aean  30307  fiunelcarsg  30378  probcun  30480  probdif  30482  cndprobin  30496  climuzcnv  31565  matunitlindflem1  33405  mblfinlem1  33446  mblfinlem2  33447  ftc1anclem6  33490  ssbnd  33587  heibor1  33609  exidcl  33675  rngocl  33700  rngogcl  33711  rngocom  33712  rngoa4  33715  rngosub  33729  rngonegmn1l  33740  rngonegmn1r  33741  ispridlc  33869  lshpcmp  34275  opltcon3b  34491  oldmm1  34504  olj01  34512  latm32  34518  omllaw4  34533  omllaw5N  34534  cmtcomlemN  34535  cmt2N  34537  cmtbr2N  34540  cmtbr3N  34541  cmtbr4N  34542  glbconxN  34664  hlexch1  34668  hlexch2  34669  hlexchb1  34670  hlexchb2  34671  hlexch3  34677  hlexch4N  34678  hlatexchb1  34679  hlatexchb2  34680  hlatexch1  34681  hlatexch2  34682  hlatle  34684  hlateq  34685  hlrelat1  34686  hlrelat2  34689  cvr1  34696  cvrval5  34701  cvrp  34702  atcvr1  34703  atcvr2  34704  cvrexchlem  34705  cvrexch  34706  dalem54  35012  pmaple  35047  pmap11  35048  paddass  35124  pmapj2N  35215  pmapocjN  35216  trlval2  35450  eelT00  38930  eelTTT  38931  eelT11  38932  eelT12  38934  eelTT1  38935  eelT01  38936  mullimc  39848  mullimcf  39855  stoweidlem52  40269  stoweidlem60  40277  rngcl  41883  nzerooringczr  42072  ply1mulgsum  42178  sinhpcosh  42481  reseccl  42494  recsccl  42495  recotcl  42496  onetansqsecsq  42502