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-1 5  ax-2 6  ax-mp 7

This theorem is referenced by:  imim12i  59  imim3i  61  imim21b  251  jcab  571  pm3.48  735  con1dc  792  jadc  799  pm4.78i  847  pm5.6r  875  exbir  1371  19.21h  1495  nford  1505  19.21ht  1519  exim  1536  i19.24  1576  equsexd  1665  equvini  1689  nfexd  1692  sbimi  1695  sbcof2  1739  nfsb2or  1766  mopick  2027  r19.32r  2515  r19.36av  2519  ceqsalt  2646  vtoclgft  2670  spcgft  2697  spcegft  2699  elab3gf  2766  mo2icl  2795  euind  2803  reu6  2805  reuind  2821  sbciegft  2870  ssddif  3234  dfiin2g  3769  invdisj  3845  ordunisuc2r  4344  fnoprabg  5760  caucvgsr  7408  rexanre  10714  elabgft1  11951  bj-nntrans  12119