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

Theorem mp3an3 1220
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 1105 . 2 ((φ ψ) → (χθ))
41, 3mpi 15 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:  mp3an13  1222  mp3an23  1223  mp3anl3  1227  opelxp  4317  funimaexg  4926  ov  5562  ovmpt2a  5573  ovmpt2  5578  ovtposg  5815  oaword1  5989  th3q  6147  enrefg  6180  f1imaen  6210  addnnnq0  6431  mulnnnq0  6432  prarloclemcalc  6484  genpelxp  6493  genpprecll  6496  genppreclu  6497  addsrpr  6633  mulsrpr  6634  gt0srpr  6636  mulid1  6782  ltneg  7212  leneg  7215  suble0  7226  div1  7422  nnaddcl  7675  nnmulcl  7676  nnge1  7678  nnsub  7693  2halves  7891  halfaddsub  7896  addltmul  7898  zleltp1  8035  nnaddm1cl  8041  zextlt  8068  peano5uzti  8082  eluzp1p1  8234  uzaddcl  8265  znq  8295  xrre  8463  xrre2  8464  fzshftral  8700  expn1ap0  8879  expadd  8911  expmul  8914  expubnd  8925  sqmul  8930  bernneq  8982  sqrecapd  8998
  Copyright terms: Public domain W3C validator