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

Theorem mp3an3 1287
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 1166 . 2 ((𝜑𝜓) → (𝜒𝜃))
41, 3mpi 15 1 ((𝜑𝜓) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  w3a 945
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116  df-3an 947
This theorem is referenced by:  mp3an13  1289  mp3an23  1290  mp3anl3  1294  opelxp  4529  funimaexg  5165  ov  5844  ovmpoa  5855  ovmpo  5860  ovtposg  6110  oaword1  6321  th3q  6488  enrefg  6612  f1imaen  6642  mapxpen  6695  xpfi  6771  djucomen  7020  addnnnq0  7205  mulnnnq0  7206  prarloclemcalc  7258  genpelxp  7267  genpprecll  7270  genppreclu  7271  addsrpr  7488  mulsrpr  7489  gt0srpr  7491  mulid1  7687  ltneg  8143  leneg  8146  suble0  8157  div1  8376  nnaddcl  8650  nnmulcl  8651  nnge1  8653  nnsub  8669  2halves  8853  halfaddsub  8858  addltmul  8860  zleltp1  9013  nnaddm1cl  9019  zextlt  9047  peano5uzti  9063  eluzp1p1  9253  uzaddcl  9283  znq  9318  xrre  9496  xrre2  9497  fzshftral  9781  expn1ap0  10196  expadd  10228  expmul  10231  expubnd  10243  sqmul  10248  bernneq  10305  sqrecapd  10321  faclbnd2  10381  faclbnd6  10383  fihashssdif  10457  shftval3  10492  caucvgre  10645  leabs  10738  ltabs  10751  caubnd2  10781  efexp  11239  efival  11290  cos01gt0  11320  odd2np1  11418  halfleoddlt  11439  omoe  11441  opeo  11442  gcdmultiple  11554  sqgcd  11563  nn0seqcvgd  11568  phiprmpw  11743  ntrin  12136  txuni2  12267  txopn  12276  xblpnfps  12387  xblpnf  12388  bl2in  12392  unirnblps  12411  unirnbl  12412  blpnfctr  12428
  Copyright terms: Public domain W3C validator