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

Theorem mp3an3 1258
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 1141 . 2 ((𝜑𝜓) → (𝜒𝜃))
41, 3mpi 15 1 ((𝜑𝜓) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  w3a 920
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115  df-3an 922
This theorem is referenced by:  mp3an13  1260  mp3an23  1261  mp3anl3  1265  opelxp  4394  funimaexg  5008  ov  5645  ovmpt2a  5656  ovmpt2  5661  ovtposg  5902  oaword1  6108  th3q  6270  enrefg  6303  f1imaen  6333  addnnnq0  6690  mulnnnq0  6691  prarloclemcalc  6743  genpelxp  6752  genpprecll  6755  genppreclu  6756  addsrpr  6973  mulsrpr  6974  gt0srpr  6976  mulid1  7167  ltneg  7622  leneg  7625  suble0  7636  div1  7847  nnaddcl  8115  nnmulcl  8116  nnge1  8118  nnsub  8133  2halves  8316  halfaddsub  8321  addltmul  8323  zleltp1  8476  nnaddm1cl  8482  zextlt  8509  peano5uzti  8525  eluzp1p1  8714  uzaddcl  8744  znq  8779  xrre  8952  xrre2  8953  fzshftral  9190  expn1ap0  9572  expadd  9604  expmul  9607  expubnd  9619  sqmul  9624  bernneq  9679  sqrecapd  9695  faclbnd2  9755  faclbnd6  9757  shftval3  9842  caucvgre  9994  leabs  10087  ltabs  10100  caubnd2  10130  odd2np1  10406  halfleoddlt  10427  omoe  10429  opeo  10430  gcdmultiple  10542  sqgcd  10551  nn0seqcvgd  10556
  Copyright terms: Public domain W3C validator