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  607  pm4.78i  790  pm3.48  793  con1dc  864  jadc  871  pm5.6r  935  exbir  1482  19.21h  1606  nford  1616  19.21ht  1630  exim  1648  i19.24  1688  equsexd  1778  equvini  1807  nfexd  1810  sbimi  1813  sbcof2  1859  nfsb2or  1886  mopick  2161  r19.32r  2691  r19.36av  2696  ceqsalt  2842  vtoclgft  2867  spcgft  2896  spcegft  2898  elab3gf  2970  mo2icl  2999  euind  3007  reu6  3009  reuind  3025  sbciegft  3076  ssddif  3459  dfiin2g  4029  invdisj  4107  ordunisuc2r  4641  fnoprabg  6162  caucvgsr  8133  rexanre  11930  tgcnp  15186  lmcvg  15194  elabgft1  16662  bj-nntrans  16833