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

Theorem mp3an23 1261
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 1258 . 2 ((𝜑𝜓) → 𝜃)
51, 4mpan2 416 1 (𝜑𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 920
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115  df-3an 922
This theorem is referenced by:  sbciegf  2856  ac6sfi  6544  1qec  6850  ltaddnq  6869  halfnqq  6872  1idsr  7217  pn0sr  7220  muleqadd  8035  halfcl  8534  rehalfcl  8535  half0  8536  2halves  8537  halfpos2  8538  halfnneg2  8540  halfaddsub  8542  nneoor  8744  zeo  8747  fztp  9385  modqfrac  9633  iexpcyc  9895  bcn2  10007  bcpasc  10009  imre  10112  reim  10113  crim  10119  addcj  10152  imval2  10155  odd2np1lem  10652  odd2np1  10653
  Copyright terms: Public domain W3C validator