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

Theorem mp3an23 1288
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 1285 . 2 ((𝜑𝜓) → 𝜃)
51, 4mpan2 419 1 (𝜑𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 943
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116  df-3an 945
This theorem is referenced by:  sbciegf  2906  ac6sfi  6743  dju0en  7015  1qec  7138  ltaddnq  7157  halfnqq  7160  1idsr  7505  pn0sr  7508  muleqadd  8336  halfcl  8844  rehalfcl  8845  half0  8846  2halves  8847  halfpos2  8848  halfnneg2  8850  halfaddsub  8852  nneoor  9051  zeo  9054  fztp  9745  modqfrac  9997  iexpcyc  10284  bcn2  10397  bcpasc  10399  imre  10510  reim  10511  crim  10517  addcj  10550  imval2  10553  sinf  11256  efi4p  11269  resin4p  11270  recos4p  11271  sinneg  11278  efival  11284  cosadd  11289  sinmul  11296  sinbnd  11304  cosbnd  11305  ef01bndlem  11308  sin01bnd  11309  cos01bnd  11310  sin01gt0  11313  cos01gt0  11314  sin02gt0  11315  odd2np1lem  11411  odd2np1  11412  mopnex  12488
  Copyright terms: Public domain W3C validator