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

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

Proof of Theorem mp3an23
StepHypRef Expression
1 mp3an23.1 . 2 𝜓
2 mp3an23.2 . . 3 𝜒
3 mp3an23.3 . . 3 ((𝜑𝜓𝜒) → 𝜃)
42, 3mp3an3 1232 . 2 ((𝜑𝜓) → 𝜃)
51, 4mpan2 409 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:  sbciegf  2816  ac6sfi  6382  1qec  6543  ltaddnq  6562  halfnqq  6565  1idsr  6910  pn0sr  6913  muleqadd  7722  halfcl  8207  rehalfcl  8208  half0  8209  2halves  8210  halfpos2  8211  halfnneg2  8213  halfaddsub  8215  nneoor  8398  zeo  8401  fztp  9041  modqfrac  9286  iexpcyc  9522  bcn2  9631  bcpasc  9633  imre  9678  reim  9679  crim  9685  addcj  9718  imval2  9721  odd2np1lem  10182  odd2np1  10183
  Copyright terms: Public domain W3C validator