ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mp2b Structured version   GIF 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  2640  onsucelsucexmidlem  4194  regexmid  4199  ordsoexmid  4220  intasym  4632  relcoi1  4772  funres11  4893  cnvresid  4895  mpt2fvex  5748  df1st2  5759  df2nd2  5760  dftpos4  5796  tposf12  5802  rec1nq  6248  halfnqq  6261  axresscn  6555  0re  6630  gtso  6699  cnegexlem2  6789
  Copyright terms: Public domain W3C validator