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  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  6726  0re  6805  gtso  6874  cnegexlem2  6964  uzn0  8244  indstr  8292  dfioo2  8593  cnrecnv  9118
  Copyright terms: Public domain W3C validator