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  1777  equvini  1806  nfexd  1809  sbimi  1812  sbcof2  1858  nfsb2or  1885  mopick  2158  r19.32r  2680  r19.36av  2685  ceqsalt  2830  vtoclgft  2855  spcgft  2884  spcegft  2886  elab3gf  2957  mo2icl  2986  euind  2994  reu6  2996  reuind  3012  sbciegft  3063  ssddif  3443  dfiin2g  4008  invdisj  4086  ordunisuc2r  4618  fnoprabg  6132  caucvgsr  8065  rexanre  11841  tgcnp  15000  lmcvg  15008  elabgft1  16476  bj-nntrans  16647