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

Theorem mp3an12 1337
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 1334 . 2 ((𝜓𝜒) → 𝜃)
51, 4mpan 424 1 (𝜒𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 979
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117  df-3an 981
This theorem is referenced by:  mp3an12i  1351  ceqsralv  2782  brelrn  4874  funpr  5282  fpm  6698  ener  6796  ltaddnq  7423  ltadd1sr  7792  map2psrprg  7821  mul02  8361  ltapi  8610  div0ap  8676  divclapzi  8721  divcanap1zi  8722  divcanap2zi  8723  divrecapzi  8724  divcanap3zi  8725  divcanap4zi  8726  divassapzi  8736  divmulapzi  8737  divdirapzi  8738  redivclapzi  8752  ltm1  8820  mulgt1  8837  recgt1i  8872  recreclt  8874  ltmul1i  8894  ltdiv1i  8895  ltmuldivi  8896  ltmul2i  8897  lemul1i  8898  lemul2i  8899  cju  8935  nnge1  8959  nngt0  8961  nnrecgt0  8974  elnnnn0c  9238  elnnz1  9293  recnz  9363  eluzsubi  9572  ge0gtmnf  9840  m1expcl2  10559  1exp  10566  m1expeven  10584  expubnd  10594  iexpcyc  10642  expnbnd  10661  expnlbnd  10662  remim  10886  imval2  10920  cjdivapi  10961  absdivapzi  11180  fprodge1  11664  ef01bndlem  11781  sin01gt0  11786  cos01gt0  11787  cos12dec  11792  absefib  11795  efieq1re  11796  zeo3  11890  evend2  11911  cnbl0  14417  reeff1olem  14575  sincosq1sgn  14630  sincosq3sgn  14632  sincosq4sgn  14633  rpelogb  14750  lgsdir2lem2  14813
  Copyright terms: Public domain W3C validator