Theorem imim2i 12

Description: Inference adding common antecedents in an implication. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
imim2i.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
imim2i	⊢ ((𝜒 → 𝜑) → (𝜒 → 𝜓))

Proof of Theorem imim2i

Step	Hyp	Ref	Expression
1		imim2i.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	a1i 9	. 2 ⊢ (𝜒 → (𝜑 → 𝜓))
3	2	a2i 11	1 ⊢ ((𝜒 → 𝜑) → (𝜒 → 𝜓))

Syntax hints:   → wi 4

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

This theorem is referenced by:  imim12i  59  imim3i  61  imim21b  253  jcab  605  pm4.78i  787  pm3.48  790  con1dc  861  jadc  868  pm5.6r  932  exbir  1479  19.21h  1603  nford  1613  19.21ht  1627  exim  1645  i19.24  1685  equsexd  1775  equvini  1804  nfexd  1807  sbimi  1810  sbcof2  1856  nfsb2or  1883  mopick  2156  r19.32r  2677  r19.36av  2682  ceqsalt  2826  vtoclgft  2851  spcgft  2880  spcegft  2882  elab3gf  2953  mo2icl  2982  euind  2990  reu6  2992  reuind  3008  sbciegft  3059  ssddif  3438  dfiin2g  3997  invdisj  4075  ordunisuc2r  4603  fnoprabg  6096  caucvgsr  7977  rexanre  11717  tgcnp  14868  lmcvg  14876  elabgft1  16072  bj-nntrans  16244