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

Theorem mp3an3 1305
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 1184 . 2 ((𝜑𝜓) → (𝜒𝜃))
41, 3mpi 15 1 ((𝜑𝜓) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  w3a 963
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116  df-3an 965
This theorem is referenced by:  mp3an13  1307  mp3an23  1308  mp3anl3  1312  opelxp  4576  funimaexg  5214  ov  5897  ovmpoa  5908  ovmpo  5913  ovtposg  6163  oaword1  6374  th3q  6541  enrefg  6665  f1imaen  6695  mapxpen  6749  xpfi  6825  djucomen  7088  addnnnq0  7280  mulnnnq0  7281  prarloclemcalc  7333  genpelxp  7342  genpprecll  7345  genppreclu  7346  addsrpr  7576  mulsrpr  7577  gt0srpr  7579  mulid1  7786  ltneg  8247  leneg  8250  suble0  8261  div1  8486  nnaddcl  8763  nnmulcl  8764  nnge1  8766  nnsub  8782  2halves  8972  halfaddsub  8977  addltmul  8979  zleltp1  9132  nnaddm1cl  9138  zextlt  9166  peano5uzti  9182  eluzp1p1  9374  uzaddcl  9407  znq  9442  xrre  9632  xrre2  9633  fzshftral  9918  expn1ap0  10333  expadd  10365  expmul  10368  expubnd  10380  sqmul  10385  bernneq  10442  sqrecapd  10458  faclbnd2  10519  faclbnd6  10521  fihashssdif  10595  shftval3  10630  caucvgre  10784  leabs  10877  ltabs  10890  caubnd2  10920  efexp  11423  efival  11473  cos01gt0  11503  odd2np1  11604  halfleoddlt  11625  omoe  11627  opeo  11628  gcdmultiple  11742  sqgcd  11751  nn0seqcvgd  11756  phiprmpw  11932  ntrin  12330  txuni2  12462  txopn  12471  xblpnfps  12604  xblpnf  12605  bl2in  12609  unirnblps  12628  unirnbl  12629  blpnfctr  12645  sincosq1eq  12966  rpcxpp1  13033  rplogb1  13071
  Copyright terms: Public domain W3C validator