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  2159  r19.32r  2689  r19.36av  2694  ceqsalt  2839  vtoclgft  2864  spcgft  2893  spcegft  2895  elab3gf  2966  mo2icl  2995  euind  3003  reu6  3005  reuind  3021  sbciegft  3072  ssddif  3454  dfiin2g  4023  invdisj  4101  ordunisuc2r  4635  fnoprabg  6153  caucvgsr  8116  rexanre  11901  tgcnp  15066  lmcvg  15074  elabgft1  16542  bj-nntrans  16713