ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mp2 GIF version

Theorem mp2 16
Description: A double modus ponens inference. (Contributed by NM, 5-Apr-1994.) (Proof shortened by Wolf Lammen, 23-Jul-2013.)
Hypotheses
Ref Expression
mp2.1 𝜑
mp2.2 𝜓
mp2.3 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
mp2 𝜒

Proof of Theorem mp2
StepHypRef Expression
1 mp2.1 . 2 𝜑
2 mp2.2 . . 3 𝜓
3 mp2.3 . . 3 (𝜑 → (𝜓𝜒))
42, 3mpi 15 . 2 (𝜑𝜒)
51, 4ax-mp 5 1 𝜒
Colors of variables: wff set class
Syntax hints:  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  impbii  125  pm3.2i  270  sstri  3076  0disj  3896  disjx0  3898  ontr2exmid  4410  0elsucexmid  4450  relres  4817  cnvdif  4915  funopab4  5130  fun0  5151  fvsn  5583  reltpos  6115  tpostpos  6129  tpos0  6139  oawordriexmid  6334  swoer  6425  xpider  6468  erinxp  6471  domfiexmid  6740  diffitest  6749  ltrel  7794  lerel  7796  frecfzennn  10167  sum0  11125  qnnen  11871  pw1dom2  13117
  Copyright terms: Public domain W3C validator