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

Theorem mp3an2 1231
 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 1115 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
41, 3mpanl2 419 1 ((𝜑𝜒) → 𝜃)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 101   ∧ w3a 896 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105 This theorem depends on definitions:  df-bi 114  df-3an 898 This theorem is referenced by:  mp3anl2  1238  ordin  4149  ordsuc  4314  omv  6065  oeiv  6066  omv2  6075  1idprl  6745  muladd11  7206  negsub  7321  subneg  7322  ltaddneg  7492  muleqadd  7722  diveqap1  7755  conjmulap  7779  nnsub  8027  addltmul  8217  zltp1le  8355  gtndiv  8392  eluzp1m1  8591  divelunit  8970  fznatpl1  9039  flqbi2  9240  flqdiv  9270  frecfzen2  9367  nn0ennn  9372  iseqshft2  9395  faclbnd3  9610  shftfvalg  9646  ovshftex  9647  shftfval  9649  abs2dif  9932  omeo  10209
 Copyright terms: Public domain W3C validator