ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  imim2i Structured version   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-1 5  ax-2 6  ax-mp 7
This theorem is referenced by:  imim12i  53  imim3i  55  imim21b  241  jcab  535  pm3.48  698  con1dc  752  jadc  759  pm4.78i  807  pm5.6r  835  exbir  1322  19.21h  1446  nford  1456  19.21ht  1470  exim  1487  i19.24  1527  equsexd  1614  equvini  1638  nfexd  1641  sbimi  1644  sbcof2  1688  nfsb2or  1715  mopick  1975  r19.32r  2451  r19.36av  2455  ceqsalt  2574  vtoclgft  2598  spcgft  2624  spcegft  2626  elab3gf  2686  mo2icl  2714  euind  2722  reu6  2724  reuind  2738  sbciegft  2787  ssddif  3165  dfiin2g  3681  invdisj  3750  ordunisuc2r  4205  fnoprabg  5544  elabgft1  9232  bj-nntrans  9385
  Copyright terms: Public domain W3C validator