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  3106  0disj  3926  disjx0  3928  ontr2exmid  4440  0elsucexmid  4480  relres  4847  cnvdif  4945  funopab4  5160  fun0  5181  fvsn  5615  reltpos  6147  tpostpos  6161  tpos0  6171  oawordriexmid  6366  swoer  6457  xpider  6500  erinxp  6503  domfiexmid  6772  diffitest  6781  ltrel  7833  lerel  7835  frecfzennn  10206  sum0  11164  qnnen  11951  pw1dom2  13220
  Copyright terms: Public domain W3C validator