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

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

Proof of Theorem mp3an1
StepHypRef Expression
1 mp3an1.1 . 2  |-  ph
2 mp3an1.2 . . 3  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
323expb 1167 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
41, 3mpan 420 1  |-  ( ( ps  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    /\ w3a 947
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116  df-3an 949
This theorem is referenced by:  mp3an12  1290  mp3an1i  1293  mp3anl1  1294  mp3an  1300  mp3an2i  1305  mp3an3an  1306  tfrlem9  6184  rdgexgg  6243  oaexg  6312  omexg  6315  oeiexg  6317  oav2  6327  nnaordex  6391  mulidnq  7165  1idpru  7367  addgt0sr  7551  muladd11  7863  cnegex  7908  negsubdi  7986  renegcl  7991  mulneg1  8125  ltaddpos  8182  addge01  8202  rimul  8315  recclap  8407  recidap  8414  recidap2  8415  recdivap2  8453  divdiv23apzi  8493  ltmul12a  8586  lemul12a  8588  mulgt1  8589  ltmulgt11  8590  gt0div  8596  ge0div  8597  ltdiv23i  8652  8th4div3  8907  gtndiv  9114  nn0ind  9133  fnn0ind  9135  xrre2  9572  ioorebasg  9726  fzen  9791  elfz0ubfz0  9870  expubnd  10318  le2sq2  10336  bernneq  10380  expnbnd  10383  faclbnd6  10458  bccl  10481  hashfacen  10547  shftfval  10561  mulreap  10604  caucvgrelemrec  10719  binom1p  11222  efi4p  11351  sinadd  11370  cosadd  11371  cos2t  11384  cos2tsin  11385  absefib  11404  efieq1re  11405  demoivreALT  11407  odd2np1  11497  opoe  11519  omoe  11520  opeo  11521  omeo  11522  gcdadd  11600  gcdmultiple  11635  algcvgblem  11657  algcvga  11659  isprm3  11726  coprm  11749  bl2ioo  12638  ioo2blex  12640  sinperlem  12816
  Copyright terms: Public domain W3C validator