ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  imim2i GIF version

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
StepHypRef Expression
1 imim2i.1 . . 3 (𝜑𝜓)
21a1i 9 . 2 (𝜒 → (𝜑𝜓))
32a2i 11 1 ((𝜒𝜑) → (𝜒𝜓))
Colors of variables: wff set class
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  577  jcn  626  pm4.78i  756  pm3.48  759  con1dc  826  jadc  833  pm5.6r  897  exbir  1397  19.21h  1521  nford  1531  19.21ht  1545  exim  1563  i19.24  1603  equsexd  1692  equvini  1716  nfexd  1719  sbimi  1722  sbcof2  1766  nfsb2or  1793  mopick  2055  r19.32r  2555  r19.36av  2559  ceqsalt  2686  vtoclgft  2710  spcgft  2737  spcegft  2739  elab3gf  2807  mo2icl  2836  euind  2844  reu6  2846  reuind  2862  sbciegft  2911  ssddif  3280  dfiin2g  3816  invdisj  3893  ordunisuc2r  4400  fnoprabg  5840  caucvgsr  7578  rexanre  10960  tgcnp  12305  lmcvg  12313  elabgft1  12912  bj-nntrans  13076
  Copyright terms: Public domain W3C validator