Theorem syl6 23

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	syl3 18	. 2 ⊢ ((ψ → χ) → (ψ → θ))
4	1, 3	syl 12	1 ⊢ (φ → (ψ → θ))

Syntax hints:   → wi 2

This theorem is referenced by:  syl7 24  syl8 25  com34 36  syldd 50  looinv 77  pm2.36 91  pm2.61 109  ja 118  syl6ib 185  syl6ibr 186  syl6bi 187  syl6bir 188  jao 274  pm4.71 481  pclem6 555  dedlemb 570  oplem1 578  3jao 632  meredith 644  hbimd 787  hbald 790  hbexd 791  19.21g 792  eqs1 828  eqs2 829  a4a 842  cbv1 845  cbv2 846  sb3 860  sb6y 872  hbsb2 873  sbn1 880  sbi1 884  sbied 903  hbsb4 905  sb9i 920  sbal1 996  mo 1020  moexex 1058  2eu1 1067  ra42 1245  rgen2 1248  mo2icl 1434  zfaus 1480  elpw2g 1803  sssn 1852  opth 1898  ss2iun 2005  iineq2 2007  trel 2048  frirr 2176  fr2nr 2177  fr3nr 2178  wefrc 2195  tz7.7 2224  onfr 2237  ordsson 2242  ssorduni 2249  ordunidif 2260  oneqmini 2272  suceloni 2314  limsuclem 2360  ordzsl 2366  tfinds 2401  ssnlim 2407  brrelex 2446  weinxp 2467  relss 2480  imasn 2616  funcnvuni 2706  fnex 2740  funrnex 2743  fv3 2839  tz6.12-2 2845  ndmfv 2848  cleqfv 2880  chfnrn 2885  ffnfv 2892  fconstfv 2903  isomin 2937  isofrlem 2939  isowe 2941  f1oweOLD 2944  iunon 2947  iinon 2948  tfrlem1 2949  tfr3 2964  rdglim2 2987  tz7.48lem 2993  tz7.49 2997  abianfp 3000  oawordex 3159  oa00 3161  oaass 3163  nnmord 3189  omsmolem 3195  omsmo 3196  ereldm 3222  erdisj 3223  eceqopreq 3249  en3d 3304  fundmen 3333  sbthbg 3360  sdomdomtr 3370  domsdomtr 3374  mapenlem2 3385  nneneq 3408  php 3409  php3 3411  onomeneq 3414  pssinf 3422  pssnn 3428  unblem1 3431  unbnn2 3436  fiint 3445  preleq 3454  inf0 3457  inf3lem2 3465  inf3lem3 3466  inf3lem5 3468  inf3lem6 3469  zfregs 3491  r1tr 3498  r1ord2 3500  tz9.12lem3 3505  rankr1lem 3517  rankr1 3518  rankval3 3525  bndrank 3526  r1pwcl 3530  cplem1 3545  karden 3551  aceq5lem4 3561  aceq5lem5 3562  aceq5 3563  aceq6b 3565  kmlem12 3591  weth 3602  zornlem4 3606  zornlem6 3608  imadomg 3616  hta 3619  carden 3638  carddom 3642  sucdom 3648  carduni 3664  cardmin 3666  alephordlem2 3678  alephordi 3679  cardinfima 3696  cfub 3703  cflim 3704  cfsuc 3709  axextnd 3737  addclpi 3814  indpi 3828  ltbtwnpq 3878  genpss 3901  genpnmax 3904  distrlem1pr 3921  ltaddpr 3934  reclem3pr 3952  reclem4pr 3953  suplem1pr 3955  suplem2pr 3956  ssgt0sr 4011  suppsrlem 4015  suppsr2 4017  suppsr3 4018  suprelem 4053  axrecex 4079  axsup 4088  negeu 4124  receu 4215  nn2get 4438  nominpos 4509  sup2 4510  creur 4532  creui 4533  zaddclt 4590  zmulclt 4596  zltp1let 4597  uzind 4603  uzwo 4605  nnwoOLD 4608  qnegclt 4643  qbtwnre 4650  nn0opthlem2 4723  sqr2irrlem3 4779  infxpidmlem7 4939  infxpidmlem8 4940  infmap2lem1 4951  infmap2lem2 4952  chlim 5139  ocsh 5164  occllem5 5184  occllem7 5186  pjthlem12 5236  pjthu 5241  pjthu2 5242  shselt 5280  spansncol 5473  h1datom 5483  osumlem4 5533  stm1add 5686  stm1add3 5688  cvnsymt 5722  mdbr2 5728  dmdbr2 5733  atcv0eq 5767  atexch 5769  atcvat4 5775

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

metamath.org