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  522  pm3.48  686  con1dc  746  jadc  753  pm4.78i  801  pm5.6r  824  exbir  1304  19.21h  1431  nford  1441  19.21ht  1455  exim  1472  i19.24  1512  equsexd  1599  equvini  1623  nfexd  1626  sbimi  1629  sbcof2  1673  nfsb2or  1700  mopick  1960  r19.32r  2435  r19.36av  2439  ceqsalt  2557  vtoclgft  2581  spcgft  2607  spcegft  2609  elab3gf  2669  mo2icl  2697  euind  2705  reu6  2707  reuind  2721  sbciegft  2770  ssddif  3148  dfiin2g  3664  invdisj  3733  ordunisuc2r  4189  fnoprabg  5525  elabgft1  7024  bj-nntrans  7173
  Copyright terms: Public domain W3C validator