Theorem syl5 22

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

Hypotheses

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

Assertion

Ref	Expression
syl5	⊢ (φ → (θ → χ))

Proof of Theorem syl5

Step	Hyp	Ref	Expression
1		syl5.1	. 2 ⊢ (φ → (ψ → χ))
2		syl5.2	. . 3 ⊢ (θ → ψ)
3	2	syl4 19	. 2 ⊢ ((ψ → χ) → (θ → χ))
4	1, 3	syl 12	1 ⊢ (φ → (θ → χ))

Syntax hints:   → wi 2

This theorem is referenced by:  pm2.04 31  nsyli 106  pm2.61 109  syl5ib 181  syl5ibr 182  syl5bi 183  syl5bir 184  jao 274  adantrd 308  sylan2 346  pm5.18 497  prlem1 576  syl3an2 620  meredith 644  a4sd 683  hbnt 710  19.21 738  eqan 816  eq5 824  cbv2 846  sb4 861  sb6y 872  hbsb3 875  sbied 903  hbsb4 905  ddelimf2 907  ax11a 926  hbeu 1016  euimmo 1045  mopick 1054  ceqsalg 1362  cgsex2g 1368  cgsex4g 1369  cla4e2gv 1398  alexeq 1409  moeq3 1432  bisbcdv 1468  pwssun 1917  reuuni4 1959  wereu 2197  tz7.7 2224  onfr 2237  tfi 2244  tfis 2245  ordtr2 2257  ordunidif 2260  onint 2261  trsuc 2308  trsucss 2309  ordsuc 2318  sucssel 2321  suc11 2341  limomss 2378  ordom 2382  peano5 2394  tfinds 2401  vtoclrbr 2450  relssres 2596  cores 2659  funss 2682  funssres 2698  funimass2 2713  imadif 2714  fneu 2728  fnex 2740  fco 2760  fex 2771  f1dmex 2819  fvelrn 2883  funfvima2 2905  funfvima3 2906  tfrlem1 2949  tfrlem5 2953  tfrlem10 2958  tfrlem11 2959  tz7.48lem 2993  tz7.48-1 2994  tz7.49 2997  tz7.49c 2998  omordi 3164  nnmordi 3188  omsmolem 3195  omsmo 3196  mapsn 3269  f1oeng 3298  f1domg 3299  dom2d 3307  ssdomg 3311  sbthlem1 3349  nneneq 3408  php 3409  infsdomnn 3426  pssnn 3428  unblem1 3431  unblem2 3432  unbnn2 3436  isfinite2 3437  fiint 3445  sucprcreg 3451  inf3lem2 3465  inf3lem3 3466  infensuc 3484  trcl 3489  zfregs 3491  rankr1 3518  rankuni 3533  aceq5 3563  ac6lem 3575  kmlem4 3583  kmlem10 3589  kmlem11 3590  weth 3602  zornlem5 3607  zornlem6 3608  hta 3619  carden 3638  carddom 3642  sucdom 3648  sdomsdomcard 3654  ondomcard 3663  carduni 3664  alephordi 3679  alephsucdom 3685  cardaleph 3690  carduniima 3695  cfsuc 3709  axpowndlem3 3745  axregndlem1 3748  axregnd 3750  axacndlem1 3753  axacndlem2 3754  axacndlem3 3755  axacndlem4 3756  axacnd 3758  indpi 3828  ltrpq 3879  genpcd 3903  prlem934 3933  ltaddpr 3934  ltexprlem1 3936  ltexprlem2 3937  ltexprlem7 3942  ltaprlem 3944  ltapr 3945  addcanpr 3946  prlem936 3949  reclem2pr 3951  reclem3pr 3952  reclem4pr 3953  mulcmpblnr 3977  recexsrlem 4006  mulgt0sr 4008  recexsr 4010  suppsr2 4017  axsup 4088  addsubt 4151  nndiv 4453  nnunb 4520  creur 4532  creui 4533  btwnz 4613  uzwo3lem2 4615  zbtwnre 4619  qbtwnre 4650  replimt 4798  climunii 4883  infxpidmlem10 4942  infxpidmlem11 4943  infmap2lem1 4951  hlimunii 5143  chsscm 5147  chocuni 5179  occllem6 5185  occl 5188  projlem15 5207  projlem28 5220  pjthlem12 5236  shlej1t 5356  chlejb1 5397  elspansn4t 5478  spansnss2t 5480  osumlem4 5533  spansncv 5542  pjss1co 5633  pjnormss 5638  pj3s 5659  stle 5681  stcltr2 5708  mdbr3 5729  mdbr4 5730  dmdbr 5731  atom1d 5750  atcvatlem 5770  atcvat4 5775  mdsymlem2 5777  mdsymlem5 5780  mdsymlem6 5781  sumdmd 5787

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

metamath.org