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

Theorem mp3an12 1305
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 1302 . 2 ((𝜓𝜒) → 𝜃)
51, 4mpan 420 1 (𝜒𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 962
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 964
This theorem is referenced by:  mp3an12i  1319  ceqsralv  2717  brelrn  4772  funpr  5175  fpm  6575  ener  6673  ltaddnq  7215  ltadd1sr  7584  map2psrprg  7613  mul02  8149  ltapi  8398  div0ap  8462  divclapzi  8507  divcanap1zi  8508  divcanap2zi  8509  divrecapzi  8510  divcanap3zi  8511  divcanap4zi  8512  divassapzi  8522  divmulapzi  8523  divdirapzi  8524  redivclapzi  8538  ltm1  8604  mulgt1  8621  recgt1i  8656  recreclt  8658  ltmul1i  8678  ltdiv1i  8679  ltmuldivi  8680  ltmul2i  8681  lemul1i  8682  lemul2i  8683  cju  8719  nnge1  8743  nngt0  8745  nnrecgt0  8758  elnnnn0c  9022  elnnz1  9077  recnz  9144  eluzsubi  9353  ge0gtmnf  9606  m1expcl2  10315  1exp  10322  m1expeven  10340  expubnd  10350  iexpcyc  10397  expnbnd  10415  expnlbnd  10416  remim  10632  imval2  10666  cjdivapi  10707  absdivapzi  10926  ef01bndlem  11463  sin01gt0  11468  cos01gt0  11469  cos12dec  11474  absefib  11477  efieq1re  11478  zeo3  11565  evend2  11586  cnbl0  12703  sincosq1sgn  12907  sincosq3sgn  12909  sincosq4sgn  12910
  Copyright terms: Public domain W3C validator