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

Theorem mp3an23 1224
 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 1221 . 2 ((𝜑𝜓) → 𝜃)
51, 4mpan2 401 1 (𝜑𝜃)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ w3a 885 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101 This theorem depends on definitions:  df-bi 110  df-3an 887 This theorem is referenced by:  sbciegf  2794  ac6sfi  6352  1qec  6486  ltaddnq  6505  halfnqq  6508  1idsr  6853  pn0sr  6856  muleqadd  7649  halfcl  8151  rehalfcl  8152  half0  8153  2halves  8154  halfpos2  8155  halfnneg2  8157  halfaddsub  8159  nneoor  8340  zeo  8343  fztp  8940  modqfrac  9179  imre  9451  reim  9452  crim  9458  addcj  9491  imval2  9494
 Copyright terms: Public domain W3C validator