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  6432  mulnnnq0  6433  prarloclemcalc  6485  genpelxp  6494  genpprecll  6497  genppreclu  6498  addsrpr  6673  mulsrpr  6674  gt0srpr  6676  mulid1  6822  ltneg  7252  leneg  7255  suble0  7266  div1  7462  nnaddcl  7715  nnmulcl  7716  nnge1  7718  nnsub  7733  2halves  7931  halfaddsub  7936  addltmul  7938  zleltp1  8075  nnaddm1cl  8081  zextlt  8108  peano5uzti  8122  eluzp1p1  8274  uzaddcl  8305  znq  8335  xrre  8503  xrre2  8504  fzshftral  8740  expn1ap0  8919  expadd  8951  expmul  8954  expubnd  8965  sqmul  8970  bernneq  9022  sqrecapd  9038
  Copyright terms: Public domain W3C validator