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  1446  19.21h  1567  nford  1577  19.21ht  1591  exim  1609  i19.24  1649  equsexd  1739  equvini  1768  nfexd  1771  sbimi  1774  sbcof2  1820  nfsb2or  1847  mopick  2114  r19.32r  2633  r19.36av  2638  ceqsalt  2775  vtoclgft  2799  spcgft  2826  spcegft  2828  elab3gf  2899  mo2icl  2928  euind  2936  reu6  2938  reuind  2954  sbciegft  3005  ssddif  3381  dfiin2g  3931  invdisj  4009  ordunisuc2r  4525  fnoprabg  5989  caucvgsr  7815  rexanre  11243  tgcnp  14062  lmcvg  14070  elabgft1  14883  bj-nntrans  15056