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

Theorem mp3an23 1292
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 1289 . 2 ((𝜑𝜓) → 𝜃)
51, 4mpan2 421 1 (𝜑𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 947
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116  df-3an 949
This theorem is referenced by:  sbciegf  2912  ac6sfi  6760  dju0en  7038  1qec  7164  ltaddnq  7183  halfnqq  7186  1idsr  7544  pn0sr  7547  ltm1sr  7553  muleqadd  8397  halfcl  8914  rehalfcl  8915  half0  8916  2halves  8917  halfpos2  8918  halfnneg2  8920  halfaddsub  8922  nneoor  9121  zeo  9124  fztp  9826  modqfrac  10078  iexpcyc  10365  bcn2  10478  bcpasc  10480  imre  10591  reim  10592  crim  10598  addcj  10631  imval2  10634  sinf  11338  efi4p  11351  resin4p  11352  recos4p  11353  sinneg  11360  efival  11366  cosadd  11371  sinmul  11378  sinbnd  11386  cosbnd  11387  ef01bndlem  11390  sin01bnd  11391  cos01bnd  11392  sin01gt0  11395  cos01gt0  11396  sin02gt0  11397  odd2np1lem  11496  odd2np1  11497  mopnex  12601  sincosq1lem  12833  sincosq2sgn  12835  sincosq3sgn  12836  sincosq4sgn  12837  sinq12gt0  12838  abssinper  12854  coskpi  12856
  Copyright terms: Public domain W3C validator