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

Theorem mp3an3 1230
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 1115 . 2 ((𝜑𝜓) → (𝜒𝜃))
41, 3mpi 15 1 ((𝜑𝜓) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101  w3a 894
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114  df-3an 896
This theorem is referenced by:  mp3an13  1232  mp3an23  1233  mp3anl3  1237  opelxp  4399  funimaexg  5008  ov  5645  ovmpt2a  5656  ovmpt2  5661  ovtposg  5902  oaword1  6078  th3q  6239  enrefg  6272  f1imaen  6302  addnnnq0  6575  mulnnnq0  6576  prarloclemcalc  6628  genpelxp  6637  genpprecll  6640  genppreclu  6641  addsrpr  6858  mulsrpr  6859  gt0srpr  6861  mulid1  7052  ltneg  7501  leneg  7504  suble0  7515  div1  7724  nnaddcl  7980  nnmulcl  7981  nnge1  7983  nnsub  7998  2halves  8181  halfaddsub  8186  addltmul  8188  zleltp1  8327  nnaddm1cl  8333  zextlt  8360  peano5uzti  8375  eluzp1p1  8564  uzaddcl  8595  znq  8626  xrre  8804  xrre2  8805  fzshftral  9042  expn1ap0  9395  expadd  9427  expmul  9430  expubnd  9442  sqmul  9447  bernneq  9501  sqrecapd  9517  faclbnd2  9574  faclbnd6  9576  shftval3  9620  caucvgre  9772  leabs  9864  ltabs  9877  caubnd2  9907  odd2np1  10147  halfleoddlt  10169  omoe  10171  opeo  10172  nn0seqcvgd  10206
  Copyright terms: Public domain W3C validator