Theorem syl2an 287

Description: A double syllogism inference. (Contributed by NM, 31-Jan-1997.)

Hypotheses

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

Assertion

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

Proof of Theorem syl2an

Step	Hyp	Ref	Expression
1		syl2an.2	. 2 |- ( ta -> ch )
2		syl2an.1	. . 3 |- ( ph -> ps )
3		syl2an.3	. . 3 |- ( ( ps /\ ch ) -> th )
4	2, 3	sylan 281	. 2 |- ( ( ph /\ ch ) -> th )
5	1, 4	sylan2 284	1 |- ( ( ph /\ ta ) -> th )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  syl2anr  288  anim12i  336  syl2an2  583  syl2an2r  584  mp3an3an  1321  eqeqan12d  2155  sylan9eq  2192  csbcomg  3025  sylan9ss  3110  ssconb  3209  ineqan12d  3279  dfopg  3703  breqan12d  3945  opexg  4150  copsex2g  4168  ordin  4307  onin  4308  unexg  4364  eusv1  4373  opelvvg  4588  opthprc  4590  opbrop  4618  relop  4689  dmpropg  5011  unixpm  5074  funssres  5165  funinsn  5172  funtp  5176  fnco  5231  resasplitss  5302  fodmrnu  5353  relrnfvex  5439  fconst2g  5635  oveqan12d  5793  ovi3  5907  ovg  5909  f1opw2  5976  off  5994  offres  6033  iunon  6181  nnsucsssuc  6388  nnaword1  6409  ertr  6444  erex  6453  brecop  6519  ecovdi  6540  ecovidi  6541  mapvalg  6552  pmvalg  6553  pmss12g  6569  mapsn  6584  en2sn  6707  xpf1o  6738  xpen  6739  phplem4  6749  ssfilem  6769  diffitest  6781  en1eqsn  6836  sbthlem7  6851  ordiso  6921  updjud  6967  fodju0  7019  finnum  7039  pr2nelem  7047  djucomen  7072  ltsopi  7128  pitric  7129  pitri3or  7130  ltdcpi  7131  mulclpi  7136  addcompig  7137  mulcompig  7139  distrpig  7141  ltexpi  7145  ltapig  7146  ltmpig  7147  dfplpq2  7162  dfmpq2  7163  enqbreq2  7165  enqdc  7169  addcmpblnq  7175  addpipqqslem  7177  mulpipq2  7179  mulpipq  7180  mulpipqqs  7181  addclnq  7183  distrnqg  7195  ltdcnq  7205  ltrnqg  7228  enq0breq  7244  addclnq0  7259  nqnq0a  7262  nqnq0m  7263  nq0m0r  7264  distrnq0  7267  mulcomnq0  7268  genipv  7317  genplt2i  7318  genpelvl  7320  genpelvu  7321  addnqprlemrl  7365  addnqprlemru  7366  addnqprlemfl  7367  addnqprlemfu  7368  addnqpr  7369  mulnqprlemrl  7381  mulnqprlemru  7382  mulnqprlemfl  7383  mulnqprlemfu  7384  mulnqpr  7385  distrlem4prl  7392  distrlem4pru  7393  ltnqpr  7401  recexprlemloc  7439  archrecnq  7471  mulclsr  7562  1idsr  7576  00sr  7577  prsradd  7594  axmulass  7681  axdistr  7682  axcnre  7689  peano5nnnn  7700  mulid1  7763  axltadd  7834  lenlt  7840  cnegexlem3  7939  cnegex  7940  resubcl  8026  subeqrev  8138  muladd  8146  mulsub  8163  mulsub2  8164  ltaddsub2  8199  leaddsub2  8201  leltadd  8209  ltaddpos2  8215  posdif  8217  addge02  8235  mullt0  8242  recexre  8340  recextlem1  8412  recexap  8414  divmuldivap  8472  conjmulap  8489  div2subap  8596  prodgt02  8611  prodge02  8613  lemul2  8615  lemul2a  8617  ltmulgt12  8623  lemulge12  8625  ltmuldiv2  8633  ltdivmul2  8636  ledivmul2  8638  lemuldiv2  8640  negiso  8713  cju  8719  peano5nni  8723  nnaddcl  8740  nnmulcl  8741  nnsub  8759  addltmul  8956  avgle1  8960  avgle2  8961  nnrecl  8975  nn0nnaddcl  9008  zsubcl  9095  zleloe  9101  znnsub  9105  nzadd  9106  zmulcl  9107  zltp1le  9108  zleltp1  9109  nnleltp1  9113  nnltp1le  9114  nnaddm1cl  9115  nn0ltp1le  9116  nn0leltp1  9117  nn0ltlem1  9118  znn0sub  9119  nn0sub  9120  elz2  9122  zapne  9125  zdcle  9127  zdclt  9128  zltlen  9129  nn0lem1lt  9134  nnlem1lt  9135  nnltlem1  9136  zdiv  9139  zextle  9142  zextlt  9143  btwnnz  9145  prime  9150  nneo  9154  peano2uz2  9158  peano5uzti  9159  uzind  9162  fzind  9166  fnn0ind  9167  uzneg  9344  uz11  9348  eluzp1m1  9349  eluzp1p1  9351  uzin  9358  indstr  9388  uz2mulcl  9402  qre  9417  qaddcl  9427  qsubcl  9430  qltlen  9432  qlttri2  9433  irradd  9438  cnref1o  9440  rpaddcl  9465  rpmulcl  9466  rpdivcl  9467  rexadd  9635  rexsub  9636  xaddcom  9644  xnn0xadd0  9650  xnegdi  9651  elicc2  9721  iccshftr  9777  iccshftl  9779  iccdil  9781  icccntr  9783  fzval2  9793  elfz1eq  9815  peano2fzr  9817  fznlem  9821  fzsplit2  9830  fzaddel  9839  fzsubel  9840  fzrev2  9865  fzrev3  9867  uzsplit  9872  fzrevral  9885  fzrevral3  9887  fzshftral  9888  elfz2nn0  9892  fznn0sub2  9905  fz0fzdiffz0  9907  elfzmlbp  9909  difelfzle  9911  difelfznle  9912  1fv  9916  elfzouz2  9938  fzouzsplit  9956  elfzo0le  9962  fzonmapblen  9964  fzofzim  9965  fzoaddel2  9970  eluzgtdifelfzo  9974  elfzodifsumelfzo  9978  ubmelm1fzo  10003  fzofzp1b  10005  fzosplitprm1  10011  fzostep1  10014  subfzo0  10019  qbtwnxr  10035  flqbi2  10064  divfl0  10069  flqzadd  10071  flqmulnn0  10072  addmodidr  10146  modfzo0difsn  10168  frec2uzltd  10176  frec2uzrand  10178  frecfzen2  10200  seq3split  10252  seq3caopr2  10255  exp3vallem  10294  expcllem  10304  expcl2lemap  10305  1exp  10322  expge1  10330  expadd  10335  expmul  10338  expsubap  10341  leexp1a  10348  lt2sq  10366  le2sq  10367  sumsqeq0  10371  bernneq  10412  bernneq2  10413  sq11ap  10458  facdiv  10484  faclbnd  10487  faclbnd3  10489  faclbnd6  10490  facavg  10492  bcrpcl  10499  bccmpl  10500  seq3coll  10585  shftfvalg  10590  shftf  10602  crre  10629  crim  10630  mulreap  10636  readd  10641  resub  10642  remul2  10645  imadd  10649  imsub  10650  immul2  10652  ipcnval  10658  cjsub  10664  cjreim  10675  caucvgre  10753  rexanuz  10760  rexuz3  10762  resqrexlemover  10782  resqrexlemcvg  10791  resqrexlemglsq  10794  sqrtle  10808  sqrtlt  10809  sqrt11ap  10810  sqrt11  10811  absreimsq  10839  absreim  10840  absmul  10841  sqabs  10854  absdiflt  10864  absdifle  10865  abssuble0  10875  abs2difabs  10880  fzomaxdif  10885  caubnd2  10889  rpmaxcl  10995  zmaxcl  10996  minmax  11001  mincl  11002  min1inf  11003  min2inf  11004  minabs  11007  minclpr  11008  rpmincl  11009  xrmaxrecl  11024  xrminmax  11034  xrmincl  11035  xrmin1inf  11036  xrmin2inf  11037  xrminrecl  11042  xrminrpcl  11043  iooinsup  11046  climconst2  11060  climuni  11062  2clim  11070  climshft  11073  climshft2  11075  cjcn2  11085  climaddc1  11098  climmulc2  11100  climsubc1  11101  climsubc2  11102  climlec2  11110  summodclem2a  11150  zsumdc  11153  isumclim3  11192  mptfzshft  11211  fsumrev  11212  fisum0diag2  11216  telfsumo2  11236  fsumparts  11239  cvgcmpub  11245  binomlem  11252  binom1p  11254  binom1dif  11256  bcxmas  11258  isumshft  11259  expcnvap0  11271  expcnv  11273  geosergap  11275  geolim  11280  cvgratnnlemrate  11299  mertenslemi1  11304  mertenslem2  11305  mertensabs  11306  prodmodc  11347  efcj  11379  eftlub  11396  effsumlt  11398  efieq  11442  sinsub  11447  cossub  11448  subsin  11450  sinmul  11451  cosmul  11452  addcos  11453  subcos  11454  dvdssub2  11535  dvdsadd  11536  dvdsaddr  11537  dvdssub  11538  dvdssubr  11539  fzocongeq  11556  odd2np1  11570  opoe  11592  omoe  11593  opeo  11594  omeo  11595  divalgb  11622  ndvdsadd  11628  zsupcllemstep  11638  gcdabs  11676  dvdsgcd  11700  absmulgcd  11705  gcdmultiple  11708  gcdmultiplez  11709  rpmulgcd  11714  sqgcd  11717  dvdssqlem  11718  dvdssq  11719  nn0seqcvgd  11722  ialgrlemconst  11724  algrf  11726  algrp1  11727  algcvg  11729  algcvga  11732  lcmval  11744  lcmabs  11757  lcmgcd  11759  lcmdvds  11760  lcmgcdnn  11763  coprmgcdb  11769  coprmdvds  11773  coprmdvds2  11774  qredeq  11777  isprm3  11799  nprm  11804  divgcdodd  11821  prmdvdsexp  11826  sqrt2irr  11840  zgcdsq  11879  hashdvds  11897  phiprmpw  11898  crth  11900  phimullem  11901  setsvalg  11989  setsfun0  11995  restval  12126  innei  12332  cnovex  12365  txuni2  12425  txbasex  12426  txbas  12427  txtop  12429  txtopon  12431  txss12  12435  txbasval  12436  txcnp  12440  upxp  12441  txcnmpt  12442  uptx  12443  txcn  12444  txrest  12445  txdis  12446  cnmpt21  12460  hmeoco  12485  txhmeo  12488  isxmet2d  12517  blin2  12601  comet  12668  metcn  12683  txmetcn  12688  qtopbasss  12690  qtopbas  12691  remetdval  12708  bl2ioo  12711  blssioo  12714  divcnap  12724  cncfmet  12748  dvaddxxbr  12834  dvcjbr  12841  sinperlem  12889  sincosq2sgn  12908  sincosq3sgn  12909  sincos6thpi  12923  bj-inex  13105  bj-bdfindis  13145  triap  13224  cvgcmp2nlemabs  13227  trilpolemisumle  13231  inffz  13238