Theorem syl 12

Description: Syllogism inference. (A bit of trivia: this is the most commonly referenced assertion in our database. In second place is ax-mp 6, followed by visset 1350, bitr 151, imp 277, and exp 291. The Metamath program command 'show usage' shows the number of references.)

Hypotheses

Ref	Expression
syl.1	|- (ph -> ps)
syl.2	|- (ps -> ch)

Assertion

Ref	Expression
syl	|- (ph -> ch)

Proof of Theorem syl

Step	Hyp	Ref	Expression
1		syl.1	. 2 |- (ph -> ps)
2		syl.2	. . . 4 |- (ps -> ch)
3	2	a1i 7	. . 3 |- (ph -> (ps -> ch))
4	3	a2i 8	. 2 |- ((ph -> ps) -> (ph -> ch))
5	1, 4	ax-mp 6	1 |- (ph -> ch)

Syntax hints:   -> wi 2

This theorem is referenced by:  com12 13  a2d 15  syl34 20  3syl 21  syl5 22  syl6 23  syl4d 28  com23 32  pm2.43d 59  sylc 62  pm2.86d 65  a3d 70  peirce 76  nega 78  pm2.01 80  pm2.01d 81  con2d 83  con1d 85  con3d 87  con1i 88  con2i 89  con3i 90  nsyl 102  nsyl2 103  nsyl3 104  nsyl4 105  bi1 130  bi2 131  biimpd 135  biimprd 136  bitr 151  sylib 173  sylbi 174  sylibr 175  sylbir 176  orci 226  olci 227  ancld 246  ancrd 247  pm3.26d 258  pm3.27d 262  anim12i 268  jao 274  sylan 343  pm4.72 485  elimant 505  elimh 571  dedt 572  oplem1 578  3adant1 597  3adant2 598  3adant3 599  syl3an 628  syl3anc 629  meredith 644  a4s 682  a7s 689  19.20 690  19.20ii 692  19.20d 693  hbal 700  hbim 702  19.9r 718  19.12 729  19.18 732  19.21 738  19.21ai 740  19.21bi 742  19.22d 744  19.23bi 747  19.25 763  19.33b 771  biald 782  biexd 783  hbnd 786  ax9 807  eqid 810  eqcoms 813  eq4 821  eq4s 822  eq5 824  eq5s 825  eq6s 827  eqs1 828  eqsal 833  a4a 842  stdpc4 869  sbf 870  sbequi 876  bisbd 897  sbied 903  sbco3 915  a16g 933  sbal1 996  sbal2 1005  mo 1020  mo2 1026  exmoeu 1039  moexex 1058  2euex 1061  2eu2ex 1063  2eu1 1067  2eu5 1071  exists2 1073  bm1.1 1088  cleq1d 1109  cleq2d 1112  eleq1d 1155  eleq2d 1156  neeq1d 1196  neeq2d 1197  r19.22d 1276  r19.12 1281  cgsex2g 1368  cgsex4g 1369  ceqsex 1370  vtoclgf 1382  vtocleg 1390  cla4gf 1394  rcla42v 1404  rcla42ev 1405  elab3g 1420  moeq3 1432  sbcco2 1449  sbc2or 1454  elrabsf 1456  sbcel1 1466  sbcel2 1467  axrep 1473  zfrepclf 1477  nalset 1482  sseld 1506  sseq1d 1527  sseq2d 1528  psseq1d 1564  psseq2d 1565  pssssd 1568  reuss 1577  reuxfr2 1579  reuxfr 1580  reuhyp 1581  difeq1d 1587  difeq2d 1588  uneq1d 1610  uneq2d 1611  ineq1d 1644  ineq2d 1645  dedth 1784  dedth2v 1785  dedth3v 1786  elimhyp 1790  elimhyp2v 1791  elimhyp3v 1792  keephyp 1794  keephyp3v 1795  sneqd 1818  snsspr 1853  rext 1862  euabex 1869  opeq1 1876  opeq2 1877  exss 1881  dtru 1889  prex 1892  opth 1898  copsex2g 1903  opprc1 1905  opprc2 1907  opth2 1909  moop2 1910  mosubop 1911  opthwiener 1914  pwssun 1917  unieqd 1929  unisseq 1946  difex2 1951  opeluu 1953  euuni 1954  uniexb 1962  inteqd 1970  elinti 1974  intex 1986  iuneq2dv 2010  iineq2dv 2011  iinss 2025  iununi 2037  iunpw 2040  breq1d 2071  breq2d 2072  opelopabg 2115  supcl 2159  supub 2160  suplub 2161  supsn 2168  frirr 2176  ordfr 2214  ordeirr 2217  ordn2lp 2219  ordelord 2221  tz7.7 2224  ordtri3or 2230  onsst 2243  tfi 2244  ssorduni 2249  onunit 2250  uniord 2252  ordtr1 2256  ontr1 2258  ordunidif 2260  onssmin 2263  onminsb 2264  onminesb 2265  bm2.5ii 2274  onminex 2275  on0eln0 2279  0ellim 2285  suceloni 2314  onpwsuc 2315  ordnbtwn 2316  onnbtwn 2317  ordsuc 2318  ordssun 2330  ordequn 2331  ordsucun 2333  ordsucuni 2336  unon 2338  ordunisuc 2339  suc11 2341  onuninsuc 2356  onun 2358  dflim3 2368  nlimon 2369  dfom2 2374  nnord 2381  ordom 2382  nnlim 2385  peano5 2394  findes 2400  tfinds 2401  tfindsg2 2403  tfindes 2404  vtoclr 2449  vtoclibr 2451  ralxp 2456  onxpdisj 2476  relssdv 2482  xpex 2488  coeq1d 2506  coeq2d 2507  dmeqd 2533  rneqd 2557  rnss 2558  dmcoeq 2573  ssres2 2590  iss 2599  imaexg 2612  eliniseg 2618  iniseg 2619  imass1 2621  imass2 2622  xpsndisj 2655  coexg 2671  funssres 2698  fun2ssres 2699  funun 2700  fununi 2705  funcnvuni 2706  fun11uni 2707  funimacnv 2711  funimaexg 2715  fnrel 2722  fnresdm 2731  2elresin 2733  fnssres 2734  fnima 2738  fn0 2739  fnex 2740  fnopabg 2745  ffun 2754  frel 2755  fdm 2756  fss 2759  fco 2760  fssxp 2761  fcoi1 2765  fcoi2 2766  f00 2773  fconst 2774  fconstg 2775  f1eq1 2776  fornex 2793  f1of 2800  f1ofn 2801  f1ofun 2802  f1orel 2803  f1o5 2808  f1f1orn 2810  f1ocnv 2811  f1imacnv 2814  f1ococnv2 2817  f1ococnv1 2818  f1dmex 2819  f1o00 2823  fveq2 2832  fveq1d 2834  fveq2d 2836  tz6.12c 2846  nfvres 2850  fnopabfv 2858  fnsnfv 2861  funfv2 2863  fvopab2 2878  fvreseq 2882  fvrn 2888  fopab2 2891  fsn 2895  fsn2 2896  fnressn 2897  fressnfv 2898  fvconst 2899  fconst2 2902  funfvima3 2906  abrexex 2912  f1fv 2916  f1fveq 2918  f1ocnvfv1 2919  f1ocnvfv2 2920  cbvfo 2923  isorel 2932  isocnv 2934  isotr 2935  isotrALT 2936  isomin 2937  isoini 2938  isofrlem 2939  isofr 2940  isowe 2941  f1oweOLD 2944  canth 2945  iunon 2947  tfrlem2 2950  tfrlem5 2953  tfrlem6 2954  tfrlem8 2956  tfrlem9 2957  tfrlem10 2958  tfrlem11 2959  tfrlem12 2960  tfrlem13 2961  tfr3 2964  tz7.44lem1 2965  tz7.44-2 2967  tz7.44-3 2968  rdglem2 2976  rdglim2 2987  frsuc 2991  tz7.48lem 2993  tz7.48-1 2994  tz7.48-2 2995  tz7.48-3 2996  tz7.49 2997  tz7.49c 2998  abianfplem 2999  abianfp 3000  opreq1d 3012  opreq2d 3013  oprprc1 3019  cbvoprab12 3028  fnoprab 3038  oprabval 3047  oprssdm 3056  ndmoprass 3062  ndmoprdistr 3063  ndmord 3064  ndmordi 3065  caoprmo 3084  oev 3122  oa1suc 3132  oesuc 3134  oaordi 3148  oaord 3149  oacan 3150  oaword 3151  oawordri 3152  oawordeulem 3156  oawordexr 3158  oalimcl 3162  oaass 3163  omordi 3164  oen0 3165  nna0 3166  nnm0 3167  nna0r 3170  nnm0r 3171  nnarcl 3174  nnacom 3175  nndi 3180  nnmass 3181  nnmsucr 3182  nnmord 3189  nnmcan 3190  omsmo 3196  eceq2 3215  erth 3219  erthdm 3220  ecopqsi 3230  ectocl 3238  ecoptocl 3239  brecop 3242  brecop2 3243  ecopoprdm 3245  ecopoprsym 3246  eceqopreq 3249  th3qlem1 3250  th3qlem2 3251  th3q 3253  oprec 3254  ecoprcom 3255  ecoprass 3256  ecoprdi 3257  map0b 3267  mapsn 3269  mapss 3270  breng 3280  brdomg 3281  enrefg 3294  domrefg 3297  f1domg 3299  en2d 3303  idssen 3309  ener 3313  ensymg 3316  domtr 3320  f1imaen 3327  en0 3328  en1 3331  2dom 3332  fundmen 3333  en2sn 3336  snfi 3337  unen 3338  xpsnen 3339  xpsneng 3340  undom 3342  xpcomen 3343  xpdom2 3345  pw2en 3348  sbthlem2 3350  sbthlem4 3352  sbthlem8 3356  sbthlem10 3358  ensdomtr 3372  sdomtr 3373  domsdomtr 3374  enen1 3375  enen2 3376  domen1 3377  domen2 3378  sdomen1 3379  mapenlem2 3385  mapen 3386  mapdom1 3387  mapdom2lem 3388  mapdom2 3389  mapxpen 3390  xpmapenlem3 3393  xpmapenlem4 3394  xpmapenlem5 3395  mapunen 3397  ssenen 3399  phplem2 3404  phplem3 3405  phplem4 3406  phplem5 3407  nneneq 3408  php 3409  php2 3410  php3 3411  php5 3413  onomeneq 3414  ominf 3423  isfinite1 3425  pssnn 3428  ssfi 3430  unblem1 3431  unblem2 3432  unblem3 3433  unblem4 3434  unbnn 3435  unfilem1 3438  unfilem3 3440  unfi 3441  unfi2 3442  fiint 3445  opthreg 3455  inf3lemd 3463  inf3lem5 3468  inf3lem7 3470  inf5 3472  isfinite 3480  nnsdom 3481  infensuc 3484  trcl 3489  zfregs 3491  r1tr 3498  r1ord 3499  r1ord3 3501  r1val1 3502  tz9.12lem3 3505  tz9.12 3506  tz9.13 3507  rankwflem 3509  rankon 3515  rankr1 3518  r1val2 3522  r1val3 3523  rankval3 3525  bndrank 3526  r1pw 3529  r1pwcl 3530  rankuni 3533  rankuniss 3534  rankun 3535  rankonid 3538  rankr1id 3539  ranklon 3540  scottex 3541  scott0 3542  bnd2 3549  aceq3lem 3555  aceq3 3556  aceq5lem3 3560  aceq5lem4 3561  aceq5lem5 3562  aceq6a 3564  aceq6b 3565  ac7g 3570  ac6lem 3575  ac6 3576  ac6s 3577  ac6s2 3578  kmlem1 3580  kmlem10 3589  kmlem12 3591  kmlem13 3592  numth2 3600  numthcor 3601  weth 3602  zornlem1 3603  zornlem2 3604  zornlem3 3605  zornlem4 3606  zornlem5 3607  zornlem6 3608  zornlem7 3609  zorn 3611  zorn2 3612  fodom 3613  fodomb 3615  htalem 3618  oncardval 3626  oncardon 3627  oncardid 3628  cardnn 3631  cardom 3632  oncard 3636  carden 3638  carddomi 3641  entri3 3647  unxpdomlem 3649  unxpdom2 3651  sucxpdom 3652  cardlim 3657  cardsdomel 3658  iscard 3659  ondomon 3662  ondomcard 3663  carduni 3664  cardiun 3665  cardmin 3666  alephordi 3679  alephord 3680  alephle 3689  cardaleph 3690  carduniima 3695  cardinfima 3696  cfub 3703  cflim 3704  cardcf 3706  cflecard 3707  cfle 3708  cfsuc 3709  cdafi 3730  axrepndlem1 3738  axrepndlem2 3739  axrepnd 3740  axunndlem1 3741  axunnd 3742  axpowndlem2 3744  axpowndlem3 3745  axpowndlem4 3746  axpownd 3747  axregndlem2 3749  axinfndlem1 3751  axinfnd 3752  axacndlem1 3753  axacndlem2 3754  axacndlem3 3755  axacndlem4 3756  axacndlem5 3757  axacnd 3758  zfcndinf 3764  elni2 3799  pion 3801  piord 3802  addpiord 3806  mulpiord 3807  mulclpi 3815  addnidpi 3822  indpi 3828  addcmpblnq 3846  mulcmpblnq 3847  ordpipq 3850  distrpqlem 3860  distrpq 3861  recmulpq 3864  recclpq 3866  recrecpq 3867  dmrecpq 3868  ltsopq 3869  ltapq 3870  ltmpq 3871  ltexpq 3874  halfpq 3876  ltrpq 3879  elnp 3886  genpnnp 3902  genpnmax 3904  mulclprlem 3915  distrlem4pr 3924  1idpr 3927  prlem934a 3931  prlem934b 3932  prlem934 3933  ltexprlem2 3937  ltexprlem4 3939  ltexprlem6 3941  ltexprlem7 3942  ltaprlem 3944  ltapr 3945  reclem1pr 3950  reclem2pr 3951  reclem3pr 3952  reclem4pr 3953  recexpr 3954  suplem2pr 3956  addcmpblnr 3975  mulcmpblnr 3977  ltsrpr 3980  ltsosr 3997  ltasr 4003  recexsrlem 4006  addgt0sr 4007  sqgt0sr 4009  ssgt0sr 4011  mappsrpr 4012  suppsr2 4017  suppsr3 4018  supsrlem1 4019  supsrlem2 4020  mulresr 4051  axaddcl 4066  axmulcl 4068  axmulass 4073  axdistr 4074  axrecex 4079  recnd 4099  negeqd 4138  renegcl 4171  divasst 4239  divadddivt 4264  divdivdivt 4265  redivcl 4274  leltt 4278  addge0 4324  mulge0 4335  sqge0 4344  ltaddpost 4363  ltnegcon1t 4367  lenegcon1t 4369  ltplus1t 4383  divge0 4392  lemul2 4396  ltmuldiv 4400  ledivt 4405  lerec 4411  posex 4422  nn1suc 4435  nn2get 4438  nnge1t 4439  nnrecgt0t 4447  nnleltp1t 4448  nnsub 4450  nnaddm1clt 4452  sup2 4510  suprcl 4512  suprub 4513  suprlub 4514  nnreclt 4522  rimul 4534  nn0addclt 4551  nn0mulcl 4553  nn0ltp1let 4556  nn0ltlem1 4558  nnnegz 4566  elnnz 4572  elnn0z 4574  elznn0 4576  elnnz1 4581  nn0subt 4587  nn0negz 4589  zaddclt 4590  elnn0nn 4593  znnsubt 4595  zmulclt 4596  zltp1let 4597  zlem1ltt 4599  zneo 4601  uzind 4603  uzwo 4605  uzwo2 4606  nn0ind 4612  btwnz 4613  uzwo3lem2 4615  zmax 4618  zbtwnre 4619  rebtwnz 4620  flclt 4624  flleltt 4625  flgzt 4626  flidt 4627  qbtwnre 4650  om2uzran 4655  uzrdgsuc 4659  seqlem2 4663  seqval 4665  seqsuclem 4669  seqrn 4673  expvalt 4677  exp1t 4679  expcllem 4682  discrlem2 4714  discrlem3 4715  nneo 4719  nnesq 4720  nn0opthlem2 4723  sqrval 4729  sqr0 4730  sqrlem6 4736  sqrlem12 4742  sqrlem13 4743  sqrlem17 4747  sqrlem18 4748  sqrge0 4760  sqsqr 4775  sqr2irr 4782  reclt 4796  imclt 4797  replimt 4798  reim0 4809  leabs 4852  abs3lem 4861  facp1t 4873  clim2 4881  clim0 4882  climunii 4883  ruclem4 4888  ruclem8 4892  ruclem13 4897  ruclem28 4912  ruclem39 4923  xpnnen 4927  znnenlem 4929  znnen 4930  infxpidmlem1 4933  infxpidmlem2 4934  infxpidmlem3 4935  infxpidmlem4 4936  infxpidmlem5 4937  infxpidmlem7 4939  infxpidmlem8 4940  infxpidmlem10 4942  infxpidmlem11 4943  infxpidmlem12 4944  infunabs 4946  infcdaabs 4947  infdif 4948  infmap2lem1 4951  infmap2lem2 4952  infmap2 4953  alephexp1 4954  alephsuc3 4955  alephexp2 4956  gch-kn 4957  hvsub4t 5014  his2subt 5052  hiidrclt 5053  hizer1t 5054  hiidge0t 5056  hi2eqt 5059  hial2eqt 5060  normgt0t 5078  normpyct 5093  norm3lem 5096  bcs 5101  hcauchy 5103  hlim2 5112  shsubclt 5125  ch0 5133  chss 5134  chlim 5139  hlim0 5140  hlimcaui 5141  hlimunii 5143  chsscm 5147  chcmh 5148  chcompl 5150  shocelt 5163  shocsh 5165  ocss 5166  shocss 5167  occon2t 5169  oc0 5171  shocorth 5173  ococss 5174  shococss 5175  shorth 5176  chocuni 5179  occllem4 5183  occllem6 5185  occl 5188  shocclt 5190  choclt 5191  projlem1 5193  projlem6 5198  projlem8 5200  projlem10 5202  projlem12 5204  projlem13 5205  projlem15 5207  projlem24 5216  projlem25 5217  projlem26 5218  projlem28 5220  projlem29 5221  pjthlem3 5227  pjthlem4 5228  pjthlem6 5230  pjthlem7 5231  pjthlem8 5232  pjthlem9 5233  pjthlem10 5234  pjthlem11 5235  pjthlem12 5236  pjthlem14 5238  pjtht 5240  pjthut 5243  pjmvalt 5245  pjvalt 5246  axpjclt 5247  omlsilem 5249  omlsi 5250  pjpj0 5259  pjoml 5271  shselt 5280  shscl 5282  shscomt 5284  shsel1t 5286  shsvst 5288  choc1 5292  shintcl 5294  chintcl 5296  ococint 5298  dfchsup2 5299  hsupval2t 5301  hsupvalt 5302  chsupval2t 5303  chsupvalt 5304  spanclt 5305  shsupclt 5307  hsupclt 5308  chsupclt 5309  hsupss 5310  chsupsn 5313  shsupunss 5316  chsupunss 5317  spanid 5318  spanss 5319  spanssoc 5320  sshjclt 5328  shunss 5338  shslej 5339  shmod 5364  sh0let 5365  ch0let 5366  chle0t 5368  orthin 5371  chdmj1t 5442  spanun 5450  h1did 5456  h1de2b 5459  spansnsht 5466  spansnmul 5469  spansncol 5473  spansnsst 5476  spanunsn 5482  h1datom 5483  hosclt 5491  hodclt 5492  pjoml2 5495  pjoml5 5498  osumlem2 5531  osumlem3 5532  osumlem4 5533  osumlem6 5535  osumlem7 5536  osum 5538  spansncv 5542  5oalem2 5545  5oalem3 5546  5oalem5 5548  5oalem6 5549  3oalem2 5553  pjorth 5559  pjch0t 5562  pjss2 5571  pjssm 5572  pjssge0 5573  pjocin 5583  pjin 5584  pjjs 5585  pjv 5589  pjopyth 5593  hococl 5599  hosdir 5609  hoddir 5610  ho2co 5611  hoid0 5614  hoid1r 5618  pjcocl 5629  pjss1co 5633  pjnormss 5638  pjorthco 5639  pjclem1 5649  pjclem4a 5652  pjclem4 5653  pjc 5654  pjcohocl 5655  pj3lem1 5658  pj3s 5659  pjelt 5668  pjs14 5669  stjt 5676  stge1 5679  stle0 5680  stle 5681  stles 5682  stadd 5687  stadd3 5689  strlem1 5691  strlem3a 5693  strlem3 5694  strlem4 5695  strlem5 5696  str 5698  large 5700  jplem1 5701  stcltrlem1 5709  mdbr2 5728  sh1dle 5748  atom1d 5750  hatomistic 5755  chpssat 5756  chrelat2 5758  cvexchlem 5759  atcv0eq 5767  atcv1 5768  atexch 5769  atcvatlem 5770  atcvat2 5772  atcvat3 5774  atcvat4 5775  mdsymlem1 5776  mdsymlem3 5778  mdsymlem6 5781  sumdmdi 5785  sumdmdlem 5786  sumdmd 5787

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

metamath.org