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 7 1 𝜒
Colors of variables: wff set class
Syntax hints:  wi 4
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7
This theorem is referenced by:  impbii  124  pm3.2i  266  sstri  3009  0disj  3790  disjx0  3792  ontr2exmid  4276  0elsucexmid  4316  relres  4667  cnvdif  4760  funopab4  4967  fun0  4988  fvsn  5390  reltpos  5899  tpostpos  5913  tpos0  5923  oawordriexmid  6114  swoer  6200  xpiderm  6243  erinxp  6246  domfiexmid  6413  diffitest  6421  ltrel  7241  lerel  7243  frecfzennn  9508
  Copyright terms: Public domain W3C validator