NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  imim2i Unicode version

Theorem imim2i 13
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 10 . 2
32a2i 12 1
Colors of variables: wff setvar 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  53  imim3i  55  ja  153  imim21b  356  pm3.48  806  jcab  833  exbir  1365  nic-ax  1438  nic-axALT  1439  tbw-bijust  1463  merco1  1478  sbimi  1652  19.24  1662  nfimdOLD  1809  19.21hOLD  1840  19.21tOLD  1863  ax12olem3  1929  ax11indi  2196  mopick  2266  axi5r  2326  r19.36av  2759  ceqsalt  2881  vtoclgft  2905  spcgft  2931  mo2icl  3015  euind  3023  reu6  3025  reuind  3039  sbciegft  3076  dfiin2g  4000  nncaddccl  4419  fnoprabg  5585
  Copyright terms: Public domain W3C validator