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

Theorem mp3an2 1219
Description: An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.)
Hypotheses
Ref Expression
mp3an2.1 ψ
mp3an2.2 ((φ ψ χ) → θ)
Assertion
Ref Expression
mp3an2 ((φ χ) → θ)

Proof of Theorem mp3an2
StepHypRef Expression
1 mp3an2.1 . 2 ψ
2 mp3an2.2 . . 3 ((φ ψ χ) → θ)
323expa 1103 . 2 (((φ ψ) χ) → θ)
41, 3mpanl2 411 1 ((φ χ) → θ)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97   w3a 884
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110  df-3an 886
This theorem is referenced by:  mp3anl2  1226  ordin  4088  ordsuc  4241  omv  5974  oeiv  5975  omv2  5984  1idprl  6565  muladd11  6923  negsub  7035  subneg  7036  muleqadd  7411  diveqap1  7444  conjmulap  7467  nnsub  7713  addltmul  7918  zltp1le  8054  gtndiv  8091  eluzp1m1  8252  divelunit  8620  fznatpl1  8688  frecfzen2  8865  nn0ennn  8870
  Copyright terms: Public domain W3C validator