Theorem syl6 22

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

Hypotheses

Ref	Expression
syl6.1	⊢ (φ → (ψ → χ))
syl6.2	⊢ (χ → θ)

Assertion

Ref	Expression
syl6	⊢ (φ → (ψ → θ))

Proof of Theorem syl6

Step	Hyp	Ref	Expression
1		syl6.1	. 2 ⊢ (φ → (ψ → χ))
2		syl6.2	. . 3 ⊢ (χ → θ)
3	2	imim2i 17	. 2 ⊢ ((ψ → χ) → (ψ → θ))
4	1, 3	syl 10	1 ⊢ (φ → (ψ → θ))

Syntax hints:   → wi 3

This theorem is referenced by:  syl7 23  syl8 24  com34 36  a1dd 42  syldd 50  syl6com 53  looinv 83  expi 142  syl6ib 210  syl6ibr 211  syl6bi 212  syl6bir 213  jao 338  pm2.37 574  pm2.81 580  pm4.71 638  pm5.21nd 684  pclem6 746  oplem1 777  3jao 892  meredith 931  ax4 1008  hbald 1149  hbexd 1150  19.21t 1151  equs4 1187  a4imt 1195  cbv1 1199  cbv2 1200  sbied 1232  sb3 1259  dfsb2 1262  hbsb2 1264  sbn 1268  sbi1 1269  sbf3t 1285  hbsb4 1286  sb9i 1301  sbal1 1385  ax11eq 1402  ax11el 1403  ax11indn 1405  ax11indi 1406  a12stdy2 1412  mo 1432  moexex 1478  2mo 1487  2eu1 1489  ra42 1742  rgen2a 1745  mo2icl 1969  reu3 1977  csbie2t 2085  uniiunlem 2184  pwpw0 2533  sssn 2538  pwsnALT 2566  ss2iun 2645  iineq2 2647  dfiun2g 2654  trel 2761  axsep 2776  opth 2863  frirr 2954  wefrc 2970  tz7.7 3001  onfr 3014  ordunidif 3022  oneqmini 3024  suctr 3055  ralxfr 3122  ordsson 3145  ssorduni 3147  suceloni 3170  ordunisuc2 3198  tfinds 3212  ssnlim 3236  brrelex 3290  weinxp 3319  ssrel 3334  ssrelrel 3340  fv3 3844  ndmfv 3856  ssimaex 3879  chfnrn 3916  dff3 3931  dff4 3932  ffnfv 3942  fconstfv 3963  elunirnALT 3983  isomin 4013  isofrlem 4015  f1oweALT 4020  iunon 4207  iinon 4208  onfununi 4209  tfrlem1 4212  tfr3 4227  rdglim2 4250  tz7.48lem 4256  tz7.49 4260  abianfp 4263  oawordex 4327  oa00 4329  oaass 4331  oarec 4332  om00 4342  odi 4346  omass 4347  oeordi 4350  oelim2 4358  nneob 4395  omsmolem 4396  omsmo 4397  ereldm 4425  erdisj 4426  eceqopreq 4454  en3d 4542  fundmen 4569  ac6sfi 4591  sbthbg 4603  sdomdomtr 4614  domsdomtr 4621  mapenlem2 4637  nneneq 4659  php 4660  php3 4662  onomeneq 4665  pssnn 4681  unblem1 4686  fiint 4703  preleq 4748  inf3lem2 4759  inf3lem3 4760  inf3lem6 4763  zfregs 4793  r1tr 4800  r1ord2 4802  tz9.12lem3 4807  rankr1lem 4819  rankr1 4820  rankval3 4827  bndrank 4828  r1pwcl 4833  rankr1b 4845  cplem1 4866  karden 4872  hta 4874  aceq5lem4 4884  aceq5lem5 4885  aceq5 4886  aceq6b 4888  kmlem13 4923  weth 4933  zorn2lem4 4937  zorn2lem6 4939  unidom 4954  uniimadom 4956  carden 4979  carddom 4985  sucdom 4992  carduni 5008  cardmin 5010  alephordlem2 5023  alephordi 5024  cardinfima 5041  alephval2 5052  alephval3 5053  cfub 5058  cfsuc 5065  axextnd 5097  addclpi 5174  ltbtwnpq 5238  genpss 5261  genpnmax 5264  distrlem1pr 5281  ltaddpr 5294  reclem3pr 5312  reclem4pr 5313  suplem1pr 5315  suplem2pr 5316  ssgt0sr 5371  suppsrlem 5375  suppsr2 5377  suppsr3 5378  suprelem 5413  pre-axsup 5445  negeui 5509  receui 5853  nominpos 6189  lbinfm 6216  sup2 6219  infmrcl 6237  xrsupsslem 6244  xrinfmsslem 6245  supxrre 6251  supxrun 6253  supxrpnf 6256  supxrunb1 6257  supxrunb2 6258  zaddcl 6333  zmulcl 6348  zltp1le 6349  zeo 6370  uzindOLD 6379  uzwo4OLD 6381  qnegcl 6409  qbtwnre 6418  uz11 6559  uzwo 6582  uzwoOLD 6583  fsequb 6654  nn0opthlem2 6866  sqr2irrlem3 6927  seq1bndi 7113  cau5ii 7120  cvg1 7124  cvg3i 7126  cvganz 7127  caubndi 7129  bccl2 7174  fsumshftm 7235  clm3i 7282  climshfti 7307  climaddlem3 7319  climmullem8 7330  clim2serz 7337  iserzex 7338  climsupi 7358  caucvglem2 7361  caucvglem5 7364  caucvglem6 7365  expcnvlem6 7436  fsum0diaglem2 7462  elcncf 7470  ivthlem7 7492  efcltlem2 7510  efseq0ex 7516  infxpidmlem7 7770  infxpidmlem8 7771  infmap2lem1 7791  infmap2lem2 7792  tgcl 7836  basgen2 7851  elcls 7914  cnpimaex 7975  cnpco 7979  opnuni 8078  metequiv 8091  caun0 8156  lmuni 8162  lmle 8171  metelcls 8176  metcnp4 8181  xplm 8186  iscms2lem4 8203  ringideu 8387  vacnlem6 8587  minveclem27 8831  psdmrn 8910  psref 8911  psasym 8913  pstr 8914  efifolem5 8998  efif1lem3 9004  chlimi 9380  ocsh 9432  occllem6 9454  occllem7 9455  pjthlem12 9506  pjtheui 9511  shsel 9554  spansncol 9767  h1datomi 9780  osumlem4 9859  cnopc 10117  cnfnc 10134  0cnop 10182  0cnfn 10183  idcnop 10184  riesz1 10277  rnbra 10320  stm1addi 10453  stm1add3i 10455  cvnsym 10498  mdbr2 10504  dmdbr2 10511  mdsl0 10518  mdsl1i 10529  mdsl2i 10530  cvmdi 10532  atexch 10590  atcvat4i 10606  cdj1i 10642  ghomf1olem 10681  ficli 10756  domrngref 10764  domintref 10767  ref3w 10772  xrletr2 10790  prj1 10809  cljo 10834  clme 10835  fiv 10849  fiiu2 10852  lteqtpos 10880  pospos 10882  tostos 10883  ismnd2 10928  rnplrnml3 10950  ununr 10955  on1el3 10962  bsi 10995  nsn 11017  osneisi 11018  cnvhmpha 11031  hmeogrp 11044  homcard 11045  top2usne 11051  homindlem3 11053  fillsb 11073  filint 11075  efilcp 11083  efilcp2 11087  cnfilca 11088  rcfpfillem4 11092  bwt2 11123  usinuniop 11128  altretop 11144  iintlem1 11155  cmpmorp 11233  ismonc 11269  isepic 11279  idsubfun 11312  dmsdtriord 11408  elfiun 11421  ordiso 11426  ordtypelem4 11430  ordtypelem7 11433  onsdom 11437  omsubsdom 11442  omsubdom 11443  elomsubsd 11446  opncldf1 11454  cldbnd 11462  hmeoclda 11475  subntr 11482  compsublem 11487  compsub 11488  hscptsscld 11491  cncomp 11494  alexsublem2 11497  alexsublem3 11498  alexsublem4 11499  alexsub 11500  dfcon2 11501  reconnlem4 11510  reconnlem5 11511  topbasfne 11560  locfincomp 11575  comppfsc 11578  neibastop1 11579  neibastop2lem1 11580  neibastop2lem2 11581  neibastop2lem4 11583  neibastop2 11584  neibastop3 11585  topmtcl 11586  fnejoin2 11592  fbssint 11626  fbasfip 11627  fsubbas 11630  fbunfip 11631  filfinnfr 11646  filssufillem 11655  ufinffr 11663  filcon 11665  flimopn 11679  limfilcf 11683  hausfillim 11685  cnpfillim 11686  fmfnfm 11704  fclusbas 11722  fcluscomp 11733  tailfb 11762  filnetlem5 11767  ssga 11777  gaass 11781  raleqfn 11790  difxp 11798  morex 11804  ficard 11834  dif1card 11835  findcard 11836  fimax 11837  indexd 11846  indexf 11847  inficl 11849  sdclem1 11875  sdclem2 11876  incsequz 11879  fsum00 11883  fsumlt 11884  fsumlt1 11894  metsstop 11909  caushft 11916  haustlmu 11967  txbas 11973  txuni 11975  uptx 11978  txsubsp 11983  sstotbnd 11992  heiborlem1 12011  heiborlem13 12023  heiborlem15 12025  heiborlem28 12038  heiborlem29 12039  heiborlem35 12045  heiborlem41 12051  rrntotbnd 12078  phtpcdm 12103  phtpcer 12104

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

Copyright terms: Public domain