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

Theorem mp3an2 1271
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 1149 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
41, 3mpanl2 429 1 ((𝜑𝜒) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  w3a 930
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116  df-3an 932
This theorem is referenced by:  mp3anl2  1278  ordin  4245  ordsuc  4416  omv  6281  oeiv  6282  omv2  6291  1idprl  7299  muladd11  7766  negsub  7881  subneg  7882  ltaddneg  8053  muleqadd  8290  diveqap1  8326  conjmulap  8350  nnsub  8617  addltmul  8808  zltp1le  8960  gtndiv  8998  eluzp1m1  9199  xnn0le2is012  9490  divelunit  9626  fznatpl1  9697  flqbi2  9905  flqdiv  9935  frecfzen2  10041  nn0ennn  10047  faclbnd3  10330  shftfvalg  10431  ovshftex  10432  shftfval  10434  abs2dif  10718  cos2t  11255  sin01gt0  11266  cos01gt0  11267  demoivre  11276  demoivreALT  11277  omeo  11390  gcd0id  11462  sqgcd  11510  isprm3  11592  setscom  11781  setsslid  11791  setsslnid  11792
  Copyright terms: Public domain W3C validator