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  783  pm3.48  786  con1dc  857  jadc  864  pm5.6r  928  exbir  1447  19.21h  1568  nford  1578  19.21ht  1592  exim  1610  i19.24  1650  equsexd  1740  equvini  1769  nfexd  1772  sbimi  1775  sbcof2  1821  nfsb2or  1848  mopick  2120  r19.32r  2640  r19.36av  2645  ceqsalt  2786  vtoclgft  2811  spcgft  2838  spcegft  2840  elab3gf  2911  mo2icl  2940  euind  2948  reu6  2950  reuind  2966  sbciegft  3017  ssddif  3394  dfiin2g  3946  invdisj  4024  ordunisuc2r  4547  fnoprabg  6020  caucvgsr  7864  rexanre  11367  tgcnp  14388  lmcvg  14396  elabgft1  15340  bj-nntrans  15513