Theorem syl3 18

Description: Inference adding common antecedents in an implication.

Hypothesis

Ref	Expression
syl3.1	⊢ (φ → ψ)

Assertion

Ref	Expression
syl3	⊢ ((χ → φ) → (χ → ψ))

Proof of Theorem syl3

Step	Hyp	Ref	Expression
1		syl3.1	. . 3 ⊢ (φ → ψ)
2	1	a1i 7	. 2 ⊢ (χ → (φ → ψ))
3	2	a2i 8	1 ⊢ ((χ → φ) → (χ → ψ))

Syntax hints:   → wi 2

This theorem is referenced by:  syl34 20  syl6 23  syl8 25  con1 84  con3 86  impt 122  imbi2i 160  pm3.43i 235  anclb 264  ancrb 265  imdistan 339  prth 429  pm5.74 442  19.21 738  19.24 762  19.21g 792  cbv3 847  cbval 848  sbimi 854  mopick 1054  r19.36av 1299  ralcom2 1314  rcla42v 1404  mo2icl 1434  findsg 2398  tfindsg 2402  zfrep6 2744  fnopabg 2745  fopab2 2891  cbvfo 2923  tz7.48-1 2994  kmlem6 3585  kmlem11 3590  suppsr3 4018  axsup 4088  infxpidmlem12 4944  chsscm 5147  chcmh 5148

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

metamath.org