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

Theorem mp3an2 1261
Description: An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.)
Hypotheses
Ref Expression
mp3an2.1  |-  ps
mp3an2.2  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Assertion
Ref Expression
mp3an2  |-  ( (
ph  /\  ch )  ->  th )

Proof of Theorem mp3an2
StepHypRef Expression
1 mp3an2.1 . 2  |-  ps
2 mp3an2.2 . . 3  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
323expa 1143 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
41, 3mpanl2 426 1  |-  ( (
ph  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102    /\ w3a 924
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 926
This theorem is referenced by:  mp3anl2  1268  ordin  4210  ordsuc  4377  omv  6208  oeiv  6209  omv2  6218  1idprl  7139  muladd11  7605  negsub  7720  subneg  7721  ltaddneg  7892  muleqadd  8127  diveqap1  8162  conjmulap  8186  nnsub  8451  addltmul  8642  zltp1le  8794  gtndiv  8831  eluzp1m1  9032  divelunit  9409  fznatpl1  9478  flqbi2  9686  flqdiv  9716  frecfzen2  9822  nn0ennn  9828  iseqshft2  9886  faclbnd3  10139  shftfvalg  10240  ovshftex  10241  shftfval  10243  abs2dif  10527  cos2t  11028  sin01gt0  11039  cos01gt0  11040  demoivre  11049  demoivreALT  11050  omeo  11163  gcd0id  11235  sqgcd  11283  isprm3  11365
  Copyright terms: Public domain W3C validator