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

Theorem mp2b 9
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 8 . 2 ψ
4 mp2b.3 . 2 (ψχ)
53, 4ax-mp 8 1 χ
Colors of variables: wff set class
Syntax hints:  wi 4
This theorem is referenced by:  equid  1676  eqvinc  2966  intasym  5045  nfunv  5172  funres11  5200  opfv1st  5555  opfv2nd  5556  cnvpprod  5867  fvfullfunlem2  5888  fundmen  6064  xpsnen  6070  xpassen  6077  ncssfin  6172  ce0addcnnul  6200
This theorem was proved from axioms:  ax-mp 8
  Copyright terms: Public domain W3C validator