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  782  pm3.48  785  con1dc  856  jadc  863  pm5.6r  927  exbir  1436  19.21h  1557  nford  1567  19.21ht  1581  exim  1599  i19.24  1639  equsexd  1729  equvini  1758  nfexd  1761  sbimi  1764  sbcof2  1810  nfsb2or  1837  mopick  2104  r19.32r  2623  r19.36av  2628  ceqsalt  2763  vtoclgft  2787  spcgft  2814  spcegft  2816  elab3gf  2887  mo2icl  2916  euind  2924  reu6  2926  reuind  2942  sbciegft  2993  ssddif  3369  dfiin2g  3918  invdisj  3995  ordunisuc2r  4511  fnoprabg  5971  caucvgsr  7796  rexanre  11220  tgcnp  13491  lmcvg  13499  elabgft1  14301  bj-nntrans  14474