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

Theorem mp3an2 1257
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 1139 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
41, 3mpanl2 426 1 ((𝜑𝜒) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  w3a 920
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115  df-3an 922
This theorem is referenced by:  mp3anl2  1264  ordin  4176  ordsuc  4342  omv  6148  oeiv  6149  omv2  6158  1idprl  7052  muladd11  7518  negsub  7633  subneg  7634  ltaddneg  7805  muleqadd  8035  diveqap1  8070  conjmulap  8094  nnsub  8354  addltmul  8544  zltp1le  8700  gtndiv  8737  eluzp1m1  8937  divelunit  9314  fznatpl1  9383  flqbi2  9587  flqdiv  9617  frecfzen2  9723  nn0ennn  9729  iseqshft2  9767  faclbnd3  9986  shftfvalg  10080  ovshftex  10081  shftfval  10083  abs2dif  10366  omeo  10678  gcd0id  10750  sqgcd  10798  isprm3  10880
  Copyright terms: Public domain W3C validator