Theorem syl6 25

Description: A syllogism rule of inference. The second premise is used to replace the consequent of the first premise.

Hypotheses

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

Assertion

Ref	Expression
syl6	|- (ph -> (ps -> th))

Proof of Theorem syl6

Step	Hyp	Ref	Expression
1		syl6.1	. 2 |- (ph -> (ps -> ch))
2		syl6.2	. . 3 |- (ch -> th)
3	2	imim2i 11	. 2 |- ((ps -> ch) -> (ps -> th))
4	1, 3	syl 12	1 |- (ph -> (ps -> th))

Syntax hints:   -> wi 3

This theorem is referenced by:  syl7 26  syl8 27  com34 40  a1dd 53  syldd 61  syl6com 64  syl6mpi 68  looinv 99  jad 156  expi 161  syl6ib 229  syl6ibr 230  syl6bi 231  syl6bir 232  jao 367  exbiri 421  pm2.37 630  pm2.81 637  pm4.71 697  pm5.21nd 744  pclem6 813  oplem1 852  3jao 1158  meredithOLD 1201  ee22 1272  ee23 1276  orbi1r 1282  ax4 1318  hbald 1471  hbexd 1472  19.21t 1473  equs4 1510  a4imt 1519  cbv1 1523  cbv2 1524  equvini 1531  sbied 1563  sbiedOLD 1564  aev 1577  sb3 1592  dfsb2 1595  hbsb2 1597  sbn 1601  sbi1 1602  sbf3t 1619  hbsb4 1620  sb9i 1640  sbal1 1737  ax11eq 1754  ax11el 1755  ax11indn 1757  ax11indi 1758  a12stdy2 1764  mo 1787  moexex 1841  2mo 1851  2eu1 1853  ra42 2157  rgen2a 2160  rgen2aOLD 2161  mo2icl 2434  reu6 2443  csbie2t 2578  ssralv2 2674  uniiunlem 2693  sbsslem 2978  pwpw0 3134  sssn 3142  pwsnALT 3173  ss2iunOLD 3272  iineq2OLD 3275  dfiun2g 3283  dfiun2gOLD 3284  trelOLD 3419  truni 3425  axsep 3437  opth 3532  copsexg 3537  frirr 3634  wefrc 3652  tz7.7 3684  onfr 3702  ordunidif 3712  oneqmini 3714  suctr 3751  trsuc2 3754  ordsssuc2 3758  ralxfr 3839  dfwe2 3861  ordssonOLD 3868  ssorduni 3870  ssorduniOLD 3871  nlimsucg 3923  ordunisuc2 3926  tfinds 3942  tfindsOLD 3943  ssnlim 3970  brrelex 4028  weinxp 4059  ssrelOLD 4076  ssrelrelOLD 4084  xpcan 4348  xpcan2 4350  cores 4400  fv3 4690  ndmfv 4702  ssimaex 4729  chfnrn 4775  dff3 4790  dff4 4791  ffnfv 4801  fconstfv 4825  elunirnALT 4845  isomin 4876  isofrlem 4878  f1oweALT 4883  iotaval 5096  iunon 5114  iinon 5115  onfununi 5116  tfrlem1 5119  tfr3 5134  rdglim2 5157  tz7.48lem 5164  tz7.49 5168  abianfp 5171  oawordex 5239  oa00 5241  oaass 5243  oarec 5244  om00 5254  odi 5258  omass 5259  oeordi 5262  oelim2 5270  nneob 5312  omsmolem 5313  omsmo 5314  ereldm 5343  erdisj 5344  eceqopreq 5372  en3d 5460  fundmen 5487  ac6sfi 5509  sbthbg 5521  sdomdomtr 5532  domsdomtr 5539  domtriord 5546  mapenlem2 5584  nneneq 5606  php 5607  php3 5609  onomeneq 5612  pssnn 5628  unblem1 5633  fiint 5650  ordiso 5683  ordtypelem4 5687  ordtypelem7 5690  onsdom 5694  preleq 5708  inf3lem2 5720  inf3lem3 5721  inf3lem6 5724  zfregs 5754  r1tr 5765  r1ord2 5767  tz9.12lem3 5772  rankr1 5785  bndrank 5793  r1pwcl 5798  rankr1b 5810  19.21a3con13v 5828  tratrb 5831  3ax5 5832  ee233 5837  cplem1 5850  karden 5856  hta 5858  omsubsdom 5881  omsubdom 5882  elomsubsd 5885  aceq5lem4 5900  aceq5lem5 5901  aceq5 5902  aceq6b 5904  kmlem13 5939  weth 5949  zorn2lem4 5953  zorn2lem6 5955  unidom 5970  uniimadom 5972  carden 5981  carddom 5987  sucdom 5994  carduni 6010  cardmin 6012  alephordlem2 6021  alephordi 6022  cardinfima 6039  alephval2 6050  alephval3 6051  cfub 6056  cfsuc 6063  axextnd 6095  addclpi 6172  ltbtwnpq 6236  genpss 6259  genpnmax 6262  distrlem1pr 6279  ltaddpr 6292  reclem3pr 6310  reclem4pr 6311  suplem1pr 6313  suplem2pr 6314  ssgt0sr 6369  suppsrlem 6373  suppsr2 6375  suppsr3 6376  suprelem 6411  pre-axsup 6444  negeui 6510  receui 6890  nominpos 7230  lbinfm 7257  sup2 7260  infmrcl 7278  xrsupsslem 7285  xrinfmsslem 7286  supxrre 7292  supxrun 7294  supxrpnf 7297  supxrunb1 7298  supxrunb2 7299  zaddcl 7374  zmulcl 7389  zltp1le 7390  zeo 7411  uzindOLD 7420  uzwo4OLD 7422  qnegcl 7450  qbtwnre 7459  uz11 7601  uzwo 7624  uzwoOLD 7625  fsequb 7702  sqr2irrlem3 7976  seq1bndi 8162  cau5ii 8169  cvg1 8173  cvg3i 8175  cvganz 8176  caubndi 8178  bccl2 8223  fsumshftm 8292  clm3i 8339  climshfti 8364  clim2serz 8394  iserzex 8395  climsupi 8415  caucvglem2 8418  caucvglem5 8421  caucvglem6 8422  expcnvlem6 8493  fsum0diaglem2 8519  elcncf 8527  ivthlem7 8549  efcltlem2 8567  efseq0ex 8573  infxpidmlem7 8827  infxpidmlem8 8828  infmap2lem1 8848  infmap2lem2 8849  tgcl 8894  basgen2 8909  txbas 8933  txuni 8935  elcls 8980  cnpimaex 9041  cnpco 9046  opnuni 9145  metequiv 9158  caun0 9223  lmle 9238  metelcls 9243  metcnp4 9248  xplm 9253  iscms2lem4 9270  ssga 9455  gaass 9459  ringideu 9470  vacnlem6 9672  minveclem27 9916  psdmrn 9991  psref 9992  psasym 9994  pstr 9995  efifolem5 10080  efif1lem3 10086  axgroth6 10137  indexfi 10174  ficard 10176  dif1card 10177  findcardOLD 10179  fiv 10212  fiiu2 10220  uptx 10226  cnvhmpha 10240  filint 10269  fillsb 10270  fbssint 10279  fsubbas 10281  fbunfip 10282  hausfillim 10303  flimopn 10321  cncomp 10331  usinuniop 10341  ismnd2 10392  on1el3 10412  chlimi 10737  ocsh 10789  occllem6 10811  occllem7 10812  pjthlem12 10863  pjtheui 10868  shsel 10911  spansncol 11124  h1datomi 11137  osumlem4 11216  cnopc 11474  cnfnc 11491  0cnop 11540  0cnfn 11541  idcnop 11542  riesz1 11635  rnbra 11678  stm1addi 11817  stm1add3i 11819  cvnsym 11862  mdbr2 11868  dmdbr2 11875  mdsl0 11882  mdsl1i 11893  mdsl2i 11894  cvmdi 11896  atexch 11953  atcvat4i 11969  cdj1i 12005  bnj10 12374  bnj23 12397  bnj1379 13100  bnj149 13241  bnj607 13304  bnj849 13318  bnj908 13329  bnj936 13336  bnj1174 13442  bnj1280 13483  seqzresval2 13616  ghomf1olem 13637  eqreznegel 13654  negn0 13655  lbzbi 13657  suprzcl 13658  gcdcllem1 13718  algcvga 13747  isprm3 13776  truniOLD 13792  trsuc2OLD 13793  funpsstri 13835  fundmpss 13836  dfon2lem3 13851  dfon2lem4 13852  dfon2lem6 13854  dfon2lem9 13857  dfon2 13858  hbimtg 13873  tz6.26 13913  soxp 13950  frxp 13951  poseq 13954  soseq 13955  nocvxminlem 14028  nocvxmin 14029  axfelem7 14037  axfelem12 14042  axfelem15 14045  axfelem16 14046  axfelem17 14047  meran3 14237  arg-ax 14240  ficli 14353  domrngref 14364  ref4w 14370  prj1 14395  imrestr 14426  sndw 14428  injrec 14461  injrec2 14466  inpreima2 14468  inpreima5 14469  mapmapmap 14486  prjmapcp 14507  cbicplem 14508  prjnpl 14510  cljo 14534  clme 14535  domrancur1c 14550  supdef 14604  dutos1 14626  pospos 14635  tostos 14637  mgmlion 14697  clfsebs 14707  fprodadd 14713  curgrpact 14735  grpdivone 14736  fprodneg 14741  imtr 14762  rnplrnml3 14768  ununr 14769  zerdivemp1 14785  bsi 14845  intfmu2 14867  nsn 14874  osneisi 14875  hmeogrp 14892  homcard 14893  top2usne 14898  homindlem3 14900  istopx 14918  efilcp 14922  efilcp2 14926  cnfilca 14927  rcfpfillem4 14931  fbaslim2 14936  iscnp3 14946  bwt2 14960  tpgprop1 14986  altretop 14997  cntrsetlem 14999  iintlem1 15010  xrletr2 15018  lteqtpos 15024  flimfneicn 15037  lvsovso 15038  lvsovso3 15040  supexr 15043  cmpmorp 15126  dualalg 15131  dualcat2 15133  ismonc 15163  isepic 15173  idsubfun 15206  tarcrpr 15237  cptarc 15242  tarsuc2 15245  intartar 15255  intrtael 15256  tartarmap 15265  fnctartar 15284  fnctartar2 15285  dmsdtriordOLD 15360  elfiun 15369  ordisoOLD 15374  ordtypelem4OLD 15378  ordtypelem7OLD 15381  onsdomOLD 15385  omsubsdomOLD 15390  omsubdomOLD 15391  elomsubsdOLD 15394  opncldf1 15402  cldbnd 15410  hmeoclda 15421  subntr 15425  compsublem 15430  compsub 15431  hscptsscld 15434  alexsublem2 15438  alexsublem3 15439  alexsublem4 15440  alexsub 15441  dfcon2 15442  reconnlem4 15449  reconnlem5 15450  topbasfne 15499  locfincomp 15514  comppfsc 15517  neibastop1 15518  neibastop2lem1 15519  neibastop2lem2 15520  neibastop2lem4 15522  neibastop2 15523  neibastop3 15524  topmtcl 15525  fnejoin2 15531  fbasfip 15556  filfinnfr 15561  filssufillem 15570  ufinffr 15578  filcon 15580  limfilcf 15587  cnpfillim 15589  fmfnfm 15598  fclusbas 15610  fcluscomp 15621  tailfb 15639  filnetlem5 15644  raleqfn 15672  difxp 15690  fimax 15746  indexdom 15754  indexfiOLD 15755  inficl 15757  zornn0 15764  fisup2g 15768  fzmul 15790  sdclem1 15809  sdclem2 15810  incsequz 15815  fsum00 15820  fsumlt 15821  fsumlt1 15831  caushft 15851  haustlmu 15906  txsubsp 15912  sstotbnd 15936  heiborlem1 15955  heiborlem13 15967  heiborlem15 15969  heiborlem28 15982  heiborlem29 15983  heiborlem35 15989  heiborlem41 15995  rrntotbnd 16022  phtpcdm 16061  phtpcer 16062  pcohtpy 16083  zerdivemp1x 16108  ispridl2 16186  erex 16262  prtlem14 16277  prter2 16285  ax4567to6 16362  ax4567to7 16363  pm14.24 16397  sbiota1 16399  eupickbi 16400  smores 16446  smoge 16454  e2 16521  ee223 16524  sspwtrALT 16644  sspwtrALT2 16645  pwtr 16647  pwtrr 16649  suctrALT2 16661  trintALT 16705  glbconx 17029  hl2atom 17053  cvrexchlem 17059  cvratlem 17061  cvrat4 17076  ringideuNEW 17146  psubspi 17228  elpaddn0 17261  paddasslem17 17297  ispsubcl2 17356

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

Copyright terms: Public domain