Theorem syl2an 699

Description: A double syllogism inference.

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 693	. 2 |- ((ph /\ ch) -> th)
5	1, 4	sylan2 696	1 |- ((ph /\ ta) -> th)

Syntax hints:   -> wi 3   /\ wa 433

This theorem is referenced by:  syl2anOLD 708  ax11indalem 2052  eqeqan12d 2185  sylan9eq 2226  sbccomg 2790  csbcomg 2823  csbnestg 2844  sylan9ss 2890  ssconb 2989  ineqan12d 3043  ifpr 3302  breqan12d 3554  copsex2g 3734  tz7.7 3869  ordin 3873  onin 3874  ontri1 3877  onelpss 3883  onsseleq 3884  ontr2 3889  unexg 3969  euuni2 3981  eusv1 3992  eusv2OLD 3995  ordon 4040  peano4 4140  findsg 4145  vtoclr 4199  opthprc 4211  relop 4274  sotriOLD 4465  unixp 4563  coexg 4571  funco 4598  funssres 4600  funtp 4607  fnco 4658  fodmrnu 4753  resdif 4781  dffv2 4859  eqfnfv 4892  fconst2g 4952  isofrlem 5013  opreqan12d 5036  oprabval5 5091  curry1 5238  curry2 5241  soxp 5253  wexp 5254  onfununi 5293  tfrlem5 5327  tfrlem11 5333  tz7.48lem 5368  oacan 5433  oawordri 5435  oaass 5446  omord2 5449  omcan 5451  oeord 5469  oecan 5470  oeordsuc 5475  nnasuc 5483  nnmsuc 5484  nnecl 5489  nnacom 5491  nnaordi 5492  nnaword1 5502  nnmordi 5504  oaabslem 5509  oaabs 5510  omsmo 5515  brecop 5569  ecopoprtrn 5574  th3qlem1 5577  ecoprdi 5584  mapvalg 5593  pmvalg 5594  mapsn 5608  en2sn 5696  sbthlem7 5725  sbth 5729  sdomnsym 5734  domtriord 5756  xpen 5811  xpenOLD 5812  mapenlem1 5816  mapenlem2 5817  mapdom1 5820  mapdom1OLD 5821  mapdom2 5823  limenpsi 5834  phplem4 5841  php 5843  php3 5845  nndomo 5851  sucdom2 5854  1sdom 5859  unxpdom2 5865  ominf 5869  isinf 5872  pssnn 5878  en1eqsn 5884  dif1en 5886  frfi 5895  unblem2 5897  isfinite2 5902  unfilem1 5904  unfilem2 5905  unfi2 5909  unifi2 5915  fodomfi 5924  inf3lem6 6000  r111 6050  rankxplim 6124  cardnnOLD 6184  carddomi2 6190  infxpenlem 6212  omsubsuc2 6234  omsubsdom 6237  omsubdom 6238  omsubel 6239  omsubss 6240  aceq5lem4 6257  aceq8b 6265  onssnum 6272  fodomnumlem 6273  cdaval 6304  cdafi 6323  nnacda 6328  nnaun 6329  nnaun2 6330  pwsdompw 6331  coflim 6348  cflim2 6350  cofsmo 6351  coftr 6355  axcc3 6362  domtriomlem 6365  domtriomlemOLD 6366  domtriomlemOLDOLD 6369  axdc3lem2 6377  axdc3lem4 6379  axdc4lem 6381  kmlem6 6416  zorn2lem6 6440  fodom 6448  brdom6disj 6455  carddomi 6475  unxpdomlemOLD 6485  ondomcardOLD 6498  konigthlem 6504  konigthlemOLD 6506  pwcfsdom 6527  cfpwsdom 6528  nnaunOLD 6533  axrepndlem2 6540  axrepnd 6541  ltsopi 6611  mulclpi 6616  addcompi 6617  mulcompi 6619  distrpi 6621  ltexpi 6624  ltapi 6625  ltmpi 6626  addcmpblnq 6647  mulpipq 6650  addclpq 6653  addasspq 6658  distrpq 6662  ltsopq 6670  ltrpq 6680  genpnnp 6703  mulclprlem 6716  distrlem1pr 6722  distrlem5pr 6726  addcanpr 6747  reclem3pr 6753  mulcmpblnr 6778  addsrpr 6779  mulclsr 6788  mulasssr 6794  distrsr 6795  ltsosr 6798  1idsr 6802  00sr 6803  recexsrlem 6807  mulgt0sr 6809  suppsr3 6819  addcnsr 6848  axmulopr 6861  axmulass 6872  axdistr 6873  axcnre 6879  mulid1 6934  ltxrlt 6961  axltadd 6966  lenlt 6971  mul02lem1 7073  mul02 7075  cnegex 7081  muladd 7172  resubcl 7180  addsub4 7212  mulsub 7216  ltadd2 7248  leadd2 7250  ltsubadd2 7252  lesubadd2 7254  ltaddsub2 7256  leaddsub2 7258  leltadd 7270  ltaddpos2 7276  posdif 7278  addge02 7297  subge0 7298  suble0 7299  mullt0 7305  recextlem1 7308  recextlem2 7309  recex 7310  divmuldiv 7389  conjmul 7408  prodgt02 7438  prodge02 7440  lemul2 7446  lemul2OLD 7447  lemul1aOLD 7453  lemul2a 7454  lemul2aOLD 7455  ltmulgt12 7463  lemulge12 7465  ltmuldiv2 7482  ltmuldiv2OLD 7483  ltdivmulOLD 7485  ledivmulOLD 7487  ltdivmul2 7488  lt2mul2div 7489  lt2mul2divOLD 7490  ledivmul2 7491  ledivmul2OLD 7492  lemuldiv2 7494  lemuldiv2OLD 7495  lereci 7498  ledivdiv 7508  lediv2 7509  ltdiv23 7510  lediv23 7511  max1 7533  max2 7535  min1 7537  min2 7538  nnaddcl 7558  nnmulcl 7559  nnleltp1 7573  nnltp1le 7574  nnaddm1cl 7577  nndiv 7578  addltmul 7675  rpaddcl 7693  rpmulcl 7694  rpdivcl 7695  reuunineg 7727  nnrecl 7733  supxrbnd1 7756  supxrbnd2 7757  nn0nnaddcl 7788  nn0leltp1 7790  nn0ltlem1 7791  nn0sub 7823  zaddcl 7827  zsubcl 7830  znnsub 7840  znn0sub 7841  zmulcl 7843  zleltp1 7845  nn0lem1lt 7849  nnlem1lt 7850  nnltlem1 7851  zdiv 7852  z2ge 7855  zextle 7856  zextlt 7857  btwnnz 7859  prime 7862  zneo 7867  peano2uz2 7868  uzind 7872  uzindOLD 7875  uzwo4OLD 7877  fzind 7880  fnn0ind 7881  zmax 7890  rebtwnz 7892  qre 7897  qaddcl 7907  qnegcl 7908  qsubcl 7910  irradd 7915  qbtwnre 7917  qbtwnxr 7918  flge 7930  fllt 7931  flval3 7937  fladdz 7942  flzadd 7943  quoremnn0ALT 7951  quoremnn0 7952  fldiv 7955  modlt 7962  flmulnn0 7966  flmulnn0OLD 7967  modmulnn 7968  zmodcl 7969  modcyc 7974  monoord 7981  elioc2 8016  elico2 8017  elicc2 8018  icoshftf1oii 8036  snunioolem 8041  ioojoin 8043  difreicc 8044  uzneg 8057  uz11 8060  eluzp1m1 8061  eluzp1p1 8063  uzaddcl 8079  uzwo 8085  uzwoOLD 8086  indstr 8091  uz2mulcl 8098  supminf 8109  elfz1eq 8137  fzn 8138  elfz2nn0 8144  fznn0sub2 8148  fzaddel 8149  fzsubel 8150  fzopth 8151  fzsuc 8155  fzrev2 8167  fzrev3 8169  fz1eqblem 8174  fzrevral 8183  fzrevral3 8185  fzshftral 8186  fseqsupcl 8189  om2uzlti 8194  om2uzlt2i 8195  om2uzf1oi 8197  nn0ennn 8207  ser1add2i 8242  ser1addi 8243  seqzp1 8282  seqzval2 8287  seqzrn2 8294  seqzresval2g 8303  expp1 8317  expcllem 8318  expadd 8339  expmul 8340  expsub 8341  expsubOLD 8342  expordi 8345  expcan 8346  expord 8347  expwordi 8348  expmwordi 8351  lt2sq 8375  le2sq 8376  bernneq 8398  bernneqOLD 8399  bernneq2 8400  expnbnd 8401  digit2 8404  digit1 8405  sqrlem6 8428  sqrlem12 8434  sqrlei 8457  sqrlti 8458  sqr4 8467  sqr9 8468  sqr2irr 8479  crre 8519  crim 8520  mulre 8527  resub 8556  imsub 8559  cjsub 8566  cjreim 8578  cjreim2 8579  cj11OLD 8581  absreimsq 8607  absreim 8608  sqabs 8620  absdiflt 8635  absdifle 8636  abssuble0 8649  absmax 8650  abs2difabs 8656  seq1bndi 8663  cau2i 8666  cau4ii 8671  cau5i 8672  cvg1i 8673  cvg1 8674  cvg3i 8676  caubndi 8679  caurei 8680  cauimi 8681  ser1absdiflem 8682  ser1absdifi 8683  facdiv 8695  facwordi 8697  faclbnd 8698  faclbnd3 8700  faclbnd4lem4 8704  faclbnd5 8706  faclbnd6 8707  facavg 8708  bcval4 8714  bccmpl 8715  bccl2 8724  hashen 8737  hashenOLD 8739  fsum1ps 8790  fsumsplit 8792  fsumadd 8794  fsumrev 8801  fsumrev2 8802  fsumshft 8803  fsumshftm 8804  fsumcmp 8812  fsumcmpndx2 8814  fsumabs 8815  fsumabs2mul 8816  binomlem1 8838  binomlem2 8839  binomlem4 8841  binomlem5 8842  clm3i 8851  climshfti 8876  climge0 8884  climaddlem3 8888  climmullem1 8892  climmullem4 8895  climmullem5 8896  climmullem8 8899  climsub 8902  clim2serz 8906  clim2serzi 8917  climserzlei 8919  climcaui 8928  caucvglem5 8933  caucvglem6 8934  caucvgi 8935  serzf0i 8941  ser1cmp2lem 8948  ser1cmp2i 8949  cvgcmp3ci 8959  reccnv 8991  supcvglem 8992  supcvglemOLD 8994  infcvglem1OLD 8998  geoseri 9012  cvgratlem2ALT 9026  cvgratlem1 9028  cvgratlem2 9029  fsum0diaglem2 9035  fsum0diag4 9039  negfcncfi 9047  mulc1cncf 9057  ivthlem6 9064  ivthlem7 9065  ivthlem8 9066  efseq0ex 9089  efaddlem3 9118  efaddlem5 9120  efaddlem6 9121  efaddlem11 9126  efaddlem13 9128  efaddlem14 9129  efaddlem17 9132  efaddlem19 9134  abspef01tlubi 9176  reeff1o 9207  efieq 9231  sinsub 9236  cossub 9237  subsin 9239  addcos 9240  subcos 9241  xpnnenOLD 9283  znnenlem 9285  znnen 9286  rpnnen1lem5 9293  rpnnen2lem9 9303  rpnnen2lem10 9304  rpnnen2 9306  infxpidmlem1OLD 9351  infxpidmlem11OLD 9361  infxpidmlem12OLD 9362  infunabs 9364  infcdaabs 9365  infdif 9367  infxpabs 9369  infmap1 9372  infpss 9373  iunctb 9374  unctb 9376  alephmul 9382  negdvdsb 9396  dvdsnegb 9397  dvdsmul1 9401  dvdsadd 9417  dvdsaddr 9418  dvdssub 9419  dvdssubr 9420  dvdsle 9422  alzdvds 9424  divalglem0 9426  divalglem4 9429  divalglem8 9433  divalglem9 9434  divalgb 9437  divalgmod 9439  ndvdsadd 9441  gcdcllem2 9449  gcdaddm 9465  gcdabs 9467  modgcd 9468  nn0seqcvgd 9469  algcvg 9475  algcvga 9478  eucalglt 9484  mulgcdlem3 9489  mulgcdlem7 9493  mulgcd 9494  absmulgcd 9495  isprm2lem 9504  isprm3 9506  coprmdvds 9514  exprmfctlem 9516  prmdvdsexpb 9520  infpnlem1 9524  infpn2 9527  prmunb 9528  1arithlem4 9533  1arithlem5 9534  1arithlem9 9538  1arithlem11 9540  1arithlem16 9545  1arithlem20 9549  1arithlem23 9553  zaddablx 9656  lubel 9831  subbas 9915  subtop 9917  retopbas 9932  txuni 9944  neiint 10010  innei 10028  islp2 10039  iscn 10050  iscnp 10052  cnco 10061  cnconst 10073  sncld 10080  metxplem1 10119  metxplem2 10120  metxp 10127  bl2in 10136  opnin 10162  metcnp 10181  metcn 10183  cncfmet 10199  remetdval 10202  bl2ioo 10205  ioo2bl 10206  blssioo 10207  tgioolem 10208  lmuni 10245  caussi 10248  causs 10249  lmle 10254  xplm 10271  xpcn 10272  bcthlem8 10302  bcthlem9 10303  bcthlem18 10312  bcthlem20 10314  bcthlem21 10315  gxnn0suc 10408  gxnn0add 10418  gxadd 10419  gxsub 10420  gxnn0mul 10421  gxmul 10422  gxmodid 10423  abldivdiv4 10438  ablmul 10460  ghgrpilem1 10462  ghsubgi 10467  gacan 10481  vcoprnelem 10550  vacnlem3 10690  sqcn 10695  nmcnilem 10697  sm1cnilem 10707  nvo00 10784  nmoge0 10790  nmorepnf 10791  nmolb 10794  nmoub3i 10796  blocnilem 10827  blocni 10828  cnph 10842  ipasslem1 10854  ipasslem2 10855  ipasslem4 10857  ipasslem8 10861  ipasslem11 10864  ipblnfi 10880  phoeqi 10882  ajval 10886  ubthlem7 10901  ubthlem8 10902  ubthlem9 10903  ubthlem10 10904  ubthlem11 10905  ubthlem12 10906  ubthlem12OLD 10907  ubthlem13 10908  ubthlem13OLD 10909  ubthlem14 10910  minveclem9 10921  minveclem16 10930  minveclem18 10932  minveclem19 10933  minveclem21 10935  minveclem24 10938  minveclem25 10939  minveclem26 10940  minveclem27 10941  minveclem28 10942  minveclem30 10944  minveclem31 10945  minveclem36 10952  minveclem38 10954  minveceu 10955  htthlem6 10999  htthlem8 11001  pilem2 11048  pilem3 11049  pigt2lt4 11051  sincosq1sgn 11080  sincosq2sgn 11081  sincosq3sgn 11082  sincosq4sgn 11083  sinq12gt0t 11084  sincosq1eq 11086  sincos6thpi 11088  cosh111lem1 11095  efgh 11099  efifolem1 11103  efifolem2 11104  efifolem3 11105  efifolem4 11106  efifolem5 11107  efifolem6 11108  efifolem7 11109  efif1lem1 11111  efif1lem3 11113  efif1lem4 11114  eff1i 11125  relogeftb 11146  relogoprlem 11150  relogexp 11155  grothac 11166  elghomlem1 11183  tx1cn 11216  tx2cn 11217  upxp 11218  uptx 11219  txcnopab 11221  homeofval 11227  subcld 11250  filmapss 11305  flimff 11313  hvsub4 11534  his7 11584  his2sub2 11587  hial2eq2 11601  normpyc 11640  hhph 11672  bcs2 11676  hcau2 11682  hhssabli 11757  hhssnv 11759  hhsscms 11775  ocorth 11789  chocunii 11797  projlem2 11812  projlem26 11836  projlem28 11838  projlem31 11841  pjtheu2i 11875  pjpj0i 11880  shsel3 11904  shscli 11906  chsupss 11935  shjval 11946  chjval 11947  shjcl 11953  chjcl 11954  shsleji 11963  chslej 12046  chjcom 12054  chub1 12055  chdmj1 12077  spanunsni 12127  spanpr 12128  fh1 12184  fh2 12185  cm2j 12186  osumlem2 12204  osumlem3 12205  spansncvi 12222  5oalem1 12224  5oalem3 12226  5oalem5 12228  3oalem2 12233  pjvi 12275  pjds3i 12283  hoaddcl 12311  hoeq 12313  hoadddi 12356  hoadddir 12357  hosubdi 12361  hosub4 12366  hoeq1 12383  hoeq2 12384  counop 12472  adjeq 12486  brafnmul 12502  lnopsubi 12525  hmops 12572  hmopm 12573  hmopd 12574  hmopco 12575  nmcopexlem1 12578  nmcopexlem3 12580  nmcopexlem5 12582  nmcopexlem6 12583  lnopconi 12590  lnfnsubi 12602  nmcfnexlem1 12607  nmcfnexlem3 12609  nmcfnexlem5 12611  nmcfnexlem6 12612  lnfnconi 12617  nlelshi 12620  riesz3i 12622  riesz1 12625  cnlnadjlem2 12628  cnlnadjlem6 12632  cnlnssadj 12640  adjlnop 12646  adjmul 12652  adjadd 12653  nmopcoi 12655  cnvbramul 12675  kbass2 12677  kbass4 12679  kbass6 12681  leopadd 12692  leopmul2i 12695  leoptri 12696  hmopidmchi 12712  cvcon3 12845  dmdmd 12861  mddmd 12862  ssdmd1 12874  ssdmd2 12875  cvdmd 12898  superpos 12915  chrelati 12925  atcv0eq 12940  atomli 12943  atcvatlem 12946  atcvati 12947  atcvat2i 12948  irredlem4 12954  atcvat3i 12957  atcvat4i 12958  mdsymlem2 12965  mdsymlem3 12966  mdsymlem5 12968  mdsymlem8 12971  dmdsym 12974  cdjreui 12993  cdj1i 12994  cdj3lem2b 12998  cdj3lem3 12999  cdj3lem3b 13001  cdj3i 13002  bnj563 13471  bnj565 13473  bnj924 13762  bnj1116 13857  bnj554 14208  bnj557 14210  bnj569 14216  bnj594 14229  bnj953 14272  bnj1178 14375  enqbreq2 14525  nqereu 14532  nqereq 14538  addpipqNEW 14540  addpqnq 14541  mulpipqNEW 14543  mulpqnq 14544  addpqf 14547  addclnq 14548  mulpqf 14549  mulclnq 14550  adderpq 14559  mulerpq 14560  ltsonq 14572  lterpq 14573  ltbtwnnq 14581  ltrnq 14582  prlem934NEW 14592  prmdvdsexpbOLD 14602  hashgadd 14605  hashun 14606  hashxplem 14608  cayleylem2 14626  sindivcvglem4 14636  zmodid2 14651  zmodfz 14652  dfon2lem4 14733  omssadd 14745  tz6.26 14805  frxpOLD 14851  poseq 14854  soseq 14855  wfrlem10 14866  frrlem3 14883  frrlem4 14884  axdenselem4 14938  axdenselem5 14939  axfelem2 14947  axfelem20 14965  uninqs 15309  elo 15311  domintrefb 15338  surrc2 15361  unpde2eg2 15379  infxpg 15395  celsor 15416  injrec 15434  ab2rexexg 15444  rzrlzreq 15692  reacomsmgrp1 15699  reacomsmgrp4 15702  unint2t 15880  intfmu2 15881  osneisi 15893  fgsb 15948  fgsb2 15952  limfillem2 15966  limptlimpr2lem2 15985  dtt2 15990  altretop 16049  dmse1 16054  trran 16067  cnvtr 16069  1ded 16140  1cat 16161  dualcat2 16188  ismonc 16218  idsubfun 16261  isseg1 16375  dmsdtriordOLD 16445  fictb 16456  omsubsuc2OLD 16472  omsubsdomOLD 16475  omsubdomOLD 16476  omsubelOLD 16477  omsubssOLD 16478  opncldf1 16487  opnregcld 16500  cldregopn 16501  subsubtop 16508  uncomp 16518  connsub 16528  reconn 16536  ivthALT 16539  fclusff 16708  istail 16719  euuni2OLD 16748  prfunOLD 16762  cocanfo 16774  oprabvalg 16791  enf1f1o 16805  indexa 16838  frfiOLD 16856  zmodfzcl 16865  fzadd2 16876  fzsplit 16877  fzdisj 16878  fzm1 16881  sdclem2 16895  sdc 16896  incsequz 16900  incsequz2 16901  fsumlt 16906  csbrni 16917  mettrifi2 16933  geomcau 16934  iccshftr 16942  iccshftl 16944  iccdil 16946  icccntr 16948  lincmb01cmp 16963  lincmb01icc 16964  ishomeo2 16981  haustlmu 16991  lmtlm 16993  txsubsp 16997  cnresoprab 17000  txmet 17010  sstotbnd 17021  totbndbnd 17029  ismtyval 17032  isismty 17033  ismtyhmeo 17036  ismtyres 17039  heiborlem12 17051  heiborlem15 17054  heiborlem16 17055  heiborlem26 17065  heiborlem28 17067  heiborlem32 17071  heiborlem33 17072  heiborlem35 17074  heiborlem38 17077  bfplem8 17090  recms 17095  rrnmet 17101  rrndstprj2 17103  rrntotbndlem1 17105  rrntotbndlem2 17106  rrntotbnd 17107  iccbnd 17111  phtpycom 17135  phtpycolem2 17137  reparpht 17150  pcocn 17161  pcohtpylem2 17166  pcohtpy 17168  pcoass 17170  pcorevlem 17171  rnggrphom 17210  prnc 17300  ispridlc 17303  pridlc3 17306  atlatmstc 17979  hlatjidm 18027  llnneat 18214  lplnneat 18249  lplnnelln 18250  lvolneat 18292  lvolnelln 18293  lvolnelpln 18294  dalem23 18400  pointpsub 18455  linepsub 18456  pmapsub 18472  pmapglbx 18473  paddasslem14 18537  polsub 18596  pol1 18599  2polval 18602  2polss 18603  3pol 18604  2pmaplub 18612  polat 18617  2polat 18618  pnonsing 18619  polsubcl 18637  cdlemefrs29cpre1 19068

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

This theorem depends on definitions:  df-bi 232  df-an 435

Copyright terms: Public domain