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

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

Proof of Theorem mp3an3
StepHypRef Expression
1 mp3an3.1 . 2 χ
2 mp3an3.2 . . 3 ((φ ψ χ) → θ)
323expia 1092 . 2 ((φ ψ) → (χθ))
41, 3mpi 15 1 ((φ ψ) → θ)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97   w3a 873
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 875
This theorem is referenced by:  mp3an13  1208  mp3an23  1209  mp3anl3  1213  opelxp  4301  funimaexg  4909  ov  5543  ovmpt2a  5554  ovmpt2  5559  ovtposg  5796  oaword1  5965  th3q  6122  addnnnq0  6304  mulnnnq0  6305  prarloclemcalc  6356  genpelxp  6365  genpprecll  6368  genppreclu  6369  addsrpr  6492  mulsrpr  6493  gt0srpr  6495  mulid1  6626
  Copyright terms: Public domain W3C validator