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

Theorem mp3an12 1233
Description: An inference based on modus ponens. (Contributed by NM, 13-Jul-2005.)
Hypotheses
Ref Expression
mp3an12.1 𝜑
mp3an12.2 𝜓
mp3an12.3 ((𝜑𝜓𝜒) → 𝜃)
Assertion
Ref Expression
mp3an12 (𝜒𝜃)

Proof of Theorem mp3an12
StepHypRef Expression
1 mp3an12.2 . 2 𝜓
2 mp3an12.1 . . 3 𝜑
3 mp3an12.3 . . 3 ((𝜑𝜓𝜒) → 𝜃)
42, 3mp3an1 1230 . 2 ((𝜓𝜒) → 𝜃)
51, 4mpan 408 1 (𝜒𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 896
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 898
This theorem is referenced by:  mp3an12i  1247  ceqsralv  2602  brelrn  4595  funpr  4979  ener  6290  ltaddnq  6563  ltadd1sr  6919  mul02  7456  ltapi  7699  div0ap  7753  divclapzi  7798  divcanap1zi  7799  divcanap2zi  7800  divrecapzi  7801  divcanap3zi  7802  divcanap4zi  7803  divassapzi  7813  divmulapzi  7814  divdirapzi  7815  redivclapzi  7829  ltm1  7887  mulgt1  7904  recgt1i  7939  recreclt  7941  ltmul1i  7961  ltdiv1i  7962  ltmuldivi  7963  ltmul2i  7964  lemul1i  7965  lemul2i  7966  cju  7989  nnge1  8013  nngt0  8015  nnrecgt0  8027  elnnnn0c  8284  elnnz1  8325  recnz  8391  eluzsubi  8596  ge0gtmnf  8837  m1expcl2  9442  1exp  9449  m1expeven  9467  expubnd  9477  iexpcyc  9523  expnbnd  9540  expnlbnd  9541  remim  9688  imval2  9722  cjdivapi  9763  absdivapzi  9981  zeo3  10179  evend2  10201
  Copyright terms: Public domain W3C validator