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

Theorem mp3an2 1231
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 1115 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
41, 3mpanl2 419 1  |-  ( (
ph  /\  ch )  ->  th )
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  4150  ordsuc  4315  omv  6066  oeiv  6067  omv2  6076  1idprl  6746  muladd11  7207  negsub  7322  subneg  7323  ltaddneg  7493  muleqadd  7723  diveqap1  7756  conjmulap  7780  nnsub  8028  addltmul  8218  zltp1le  8356  gtndiv  8393  eluzp1m1  8592  divelunit  8971  fznatpl1  9040  flqbi2  9241  flqdiv  9271  frecfzen2  9368  nn0ennn  9373  iseqshft2  9396  faclbnd3  9611  shftfvalg  9647  ovshftex  9648  shftfval  9650  abs2dif  9933  omeo  10210
  Copyright terms: Public domain W3C validator