ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mp2b 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  2667  2ordpr  4249  regexmid  4260  ordsoexmid  4286  reg3exmid  4304  intasym  4709  relcoi1  4849  funres11  4971  cnvresid  4973  mpt2fvex  5829  df1st2  5840  df2nd2  5841  dftpos4  5878  tposf12  5884  xpcomco  6300  rec1nq  6491  halfnqq  6506  caucvgsrlemasr  6872  axresscn  6934  0re  7025  gtso  7095  cnegexlem2  7185  uzn0  8486  indstr  8534  dfioo2  8841  cnrecnv  9484  rexanuz  9561  climdm  9790
  Copyright terms: Public domain W3C validator