Theorem mp3an1 1324

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

Step	Hyp	Ref	Expression
1		mp3an1.1	. 2 |- ph
2		mp3an1.2	. . 3 |- ( ( ph /\ ps /\ ch ) -> th )
3	2	3expb 1204	. 2 |- ( ( ph /\ ( ps /\ ch ) ) -> th )
4	1, 3	mpan 424	1 |- ( ( ps /\ ch ) -> th )

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 978

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 980

This theorem is referenced by:  mp3an12  1327  mp3an1i  1330  mp3anl1  1331  mp3an  1337  mp3an2i  1342  mp3an3an  1343  tfrlem9  6319  rdgexgg  6378  oaexg  6448  omexg  6451  oeiexg  6453  oav2  6463  nnaordex  6528  mulidnq  7387  1idpru  7589  addgt0sr  7773  muladd11  8088  cnegex  8133  negsubdi  8211  renegcl  8216  mulneg1  8350  ltaddpos  8407  addge01  8427  rimul  8540  recclap  8634  recidap  8641  recidap2  8642  recdivap2  8680  divdiv23apzi  8720  ltmul12a  8815  lemul12a  8817  mulgt1  8818  ltmulgt11  8819  gt0div  8825  ge0div  8826  ltdiv23i  8881  8th4div3  9136  gtndiv  9346  nn0ind  9365  fnn0ind  9367  xrre2  9819  ioorebasg  9973  fzen  10040  elfz0ubfz0  10122  expubnd  10574  le2sq2  10592  bernneq  10637  expnbnd  10640  faclbnd6  10719  bccl  10742  hashfacen  10811  shftfval  10825  mulreap  10868  caucvgrelemrec  10983  binom1p  11488  efi4p  11720  sinadd  11739  cosadd  11740  cos2t  11753  cos2tsin  11754  absefib  11773  efieq1re  11774  demoivreALT  11776  odd2np1  11872  opoe  11894  omoe  11895  opeo  11896  omeo  11897  gcdadd  11980  gcdmultiple  12015  algcvgblem  12043  algcvga  12045  isprm3  12112  coprm  12138  1arith2  12360  cnfldneg  13398  cnfldmulg  13401  cnfldexp  13402  zringmulg  13419  zringsubgval  13426  bl2ioo  13973  ioo2blex  13975  sinperlem  14160  logge0  14232  lgsdir2  14365  1lgs  14375