ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mp2b Structured version   Unicode version

Theorem mp2b 8
Description: A double modus ponens inference. (Contributed by Mario Carneiro, 24-Jan-2013.)
Hypotheses
Ref Expression
mp2b.1
mp2b.2
mp2b.3
Assertion
Ref Expression
mp2b

Proof of Theorem mp2b
StepHypRef Expression
1 mp2b.1 . . 3
2 mp2b.2 . . 3
31, 2ax-mp 7 . 2
4 mp2b.3 . 2
53, 4ax-mp 7 1
Colors of variables: wff set class
Syntax hints:   wi 4
This theorem was proved from axioms:  ax-mp 7
This theorem is referenced by:  eqvinc  2661  onsucelsucexmidlem  4214  regexmid  4219  ordsoexmid  4240  intasym  4652  relcoi1  4792  funres11  4914  cnvresid  4916  mpt2fvex  5771  df1st2  5782  df2nd2  5783  dftpos4  5819  tposf12  5825  xpcomco  6236  rec1nq  6379  halfnqq  6393  axresscn  6746  0re  6825  gtso  6894  cnegexlem2  6984  uzn0  8264  indstr  8312  dfioo2  8613  cnrecnv  9138
  Copyright terms: Public domain W3C validator