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

Theorem mp3an2 1220
 Description: An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.)
Hypotheses
Ref Expression
mp3an2.1 𝜓
mp3an2.2 ((𝜑𝜓𝜒) → 𝜃)
Assertion
Ref Expression
mp3an2 ((𝜑𝜒) → 𝜃)

Proof of Theorem mp3an2
StepHypRef Expression
1 mp3an2.1 . 2 𝜓
2 mp3an2.2 . . 3 ((𝜑𝜓𝜒) → 𝜃)
323expa 1104 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
41, 3mpanl2 411 1 ((𝜑𝜒) → 𝜃)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97   ∧ 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:  mp3anl2  1227  ordin  4122  ordsuc  4287  omv  6035  oeiv  6036  omv2  6045  1idprl  6688  muladd11  7146  negsub  7259  subneg  7260  muleqadd  7649  diveqap1  7682  conjmulap  7705  nnsub  7952  addltmul  8161  zltp1le  8298  gtndiv  8335  eluzp1m1  8496  divelunit  8870  fznatpl1  8938  flqbi2  9133  flqdiv  9163  frecfzen2  9204  nn0ennn  9209  iseqshft2  9232  shftfvalg  9419  ovshftex  9420  shftfval  9422  abs2dif  9702
 Copyright terms: Public domain W3C validator