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

Theorem mp3an13 1306
 Description: An inference based on modus ponens. (Contributed by NM, 14-Jul-2005.)
Hypotheses
Ref Expression
mp3an13.1 𝜑
mp3an13.2 𝜒
mp3an13.3 ((𝜑𝜓𝜒) → 𝜃)
Assertion
Ref Expression
mp3an13 (𝜓𝜃)

Proof of Theorem mp3an13
StepHypRef Expression
1 mp3an13.1 . 2 𝜑
2 mp3an13.2 . . 3 𝜒
3 mp3an13.3 . . 3 ((𝜑𝜓𝜒) → 𝜃)
42, 3mp3an3 1304 . 2 ((𝜑𝜓) → 𝜃)
51, 4mpan 420 1 (𝜓𝜃)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ w3a 962 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 964 This theorem is referenced by:  pitonnlem1p1  7673  mulid1  7782  addltmul  8975  eluzaddi  9371  fz01en  9857  fznatpl1  9880  expubnd  10374  bernneq  10436  bernneq2  10437  efi4p  11447  efival  11462  cos2tsin  11481  cos01bnd  11488  cos01gt0  11492  dvds0  11531  odd2np1  11593  opoe  11615  gcdid  11697  blssioo  12740  tgioo  12741  rerestcntop  12745  sinperlem  12923  sincosq1sgn  12941  sincosq2sgn  12942  sinq12gt0  12945  cosq14gt0  12947
 Copyright terms: Public domain W3C validator