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  251  jcab  593  pm4.78i  772  pm3.48  775  con1dc  842  jadc  849  pm5.6r  913  exbir  1413  19.21h  1537  nford  1547  19.21ht  1561  exim  1579  i19.24  1619  equsexd  1708  equvini  1732  nfexd  1735  sbimi  1738  sbcof2  1783  nfsb2or  1810  mopick  2078  r19.32r  2581  r19.36av  2585  ceqsalt  2715  vtoclgft  2739  spcgft  2766  spcegft  2768  elab3gf  2838  mo2icl  2867  euind  2875  reu6  2877  reuind  2893  sbciegft  2943  ssddif  3315  dfiin2g  3854  invdisj  3931  ordunisuc2r  4438  fnoprabg  5880  caucvgsr  7634  rexanre  11024  tgcnp  12417  lmcvg  12425  elabgft1  13156  bj-nntrans  13320