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  1534  nford  1544  19.21ht  1558  exim  1576  i19.24  1616  equsexd  1706  equvini  1735  nfexd  1738  sbimi  1741  sbcof2  1787  nfsb2or  1814  mopick  2081  r19.32r  2600  r19.36av  2605  ceqsalt  2735  vtoclgft  2759  spcgft  2786  spcegft  2788  elab3gf  2858  mo2icl  2887  euind  2895  reu6  2897  reuind  2913  sbciegft  2963  ssddif  3337  dfiin2g  3878  invdisj  3955  ordunisuc2r  4467  fnoprabg  5912  caucvgsr  7701  rexanre  11097  tgcnp  12556  lmcvg  12564  elabgft1  13298  bj-nntrans  13472