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

Theorem mp3an23 1329
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 1326 . 2 ((𝜑𝜓) → 𝜃)
51, 4mpan2 425 1 (𝜑𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 978
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 980
This theorem is referenced by:  sbciegf  2994  ac6sfi  6891  dju0en  7206  1qec  7365  ltaddnq  7384  halfnqq  7387  1idsr  7745  pn0sr  7748  ltm1sr  7754  muleqadd  8601  halfcl  9121  rehalfcl  9122  half0  9123  2halves  9124  halfpos2  9125  halfnneg2  9127  halfaddsub  9129  nneoor  9331  zeo  9334  fztp  10051  modqfrac  10310  iexpcyc  10597  bcn2  10715  bcpasc  10717  imre  10831  reim  10832  crim  10838  addcj  10871  imval2  10874  sinf  11683  efi4p  11696  resin4p  11697  recos4p  11698  sinneg  11705  efival  11711  cosadd  11716  sinmul  11723  sinbnd  11731  cosbnd  11732  ef01bndlem  11735  sin01bnd  11736  cos01bnd  11737  sin01gt0  11740  cos01gt0  11741  sin02gt0  11742  odd2np1lem  11847  odd2np1  11848  pythagtriplem12  12245  pockthi  12326  mopnex  13638  sincosq1lem  13879  sincosq2sgn  13881  sincosq3sgn  13882  sincosq4sgn  13883  sinq12gt0  13884  abssinper  13900  coskpi  13902  rpcxpsqrt  13975  logsqrt  13976
  Copyright terms: Public domain W3C validator