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  603  pm4.78i  784  pm3.48  787  con1dc  858  jadc  865  pm5.6r  929  exbir  1457  19.21h  1581  nford  1591  19.21ht  1605  exim  1623  i19.24  1663  equsexd  1753  equvini  1782  nfexd  1785  sbimi  1788  sbcof2  1834  nfsb2or  1861  mopick  2133  r19.32r  2653  r19.36av  2658  ceqsalt  2800  vtoclgft  2825  spcgft  2854  spcegft  2856  elab3gf  2927  mo2icl  2956  euind  2964  reu6  2966  reuind  2982  sbciegft  3033  ssddif  3411  dfiin2g  3965  invdisj  4043  ordunisuc2r  4569  fnoprabg  6058  caucvgsr  7930  rexanre  11601  tgcnp  14751  lmcvg  14759  elabgft1  15848  bj-nntrans  16021