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

Theorem mp3an1 1302
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 1182 . 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 962
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 964
This theorem is referenced by:  mp3an12  1305  mp3an1i  1308  mp3anl1  1309  mp3an  1315  mp3an2i  1320  mp3an3an  1321  tfrlem9  6216  rdgexgg  6275  oaexg  6344  omexg  6347  oeiexg  6349  oav2  6359  nnaordex  6423  mulidnq  7204  1idpru  7406  addgt0sr  7590  muladd11  7902  cnegex  7947  negsubdi  8025  renegcl  8030  mulneg1  8164  ltaddpos  8221  addge01  8241  rimul  8354  recclap  8446  recidap  8453  recidap2  8454  recdivap2  8492  divdiv23apzi  8532  ltmul12a  8625  lemul12a  8627  mulgt1  8628  ltmulgt11  8629  gt0div  8635  ge0div  8636  ltdiv23i  8691  8th4div3  8946  gtndiv  9153  nn0ind  9172  fnn0ind  9174  xrre2  9611  ioorebasg  9765  fzen  9830  elfz0ubfz0  9909  expubnd  10357  le2sq2  10375  bernneq  10419  expnbnd  10422  faclbnd6  10497  bccl  10520  hashfacen  10586  shftfval  10600  mulreap  10643  caucvgrelemrec  10758  binom1p  11261  efi4p  11431  sinadd  11450  cosadd  11451  cos2t  11464  cos2tsin  11465  absefib  11484  efieq1re  11485  demoivreALT  11487  odd2np1  11577  opoe  11599  omoe  11600  opeo  11601  omeo  11602  gcdadd  11680  gcdmultiple  11715  algcvgblem  11737  algcvga  11739  isprm3  11806  coprm  11829  bl2ioo  12721  ioo2blex  12723  sinperlem  12902
  Copyright terms: Public domain W3C validator