Theorem mp3an1 1337

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 1207	. 2 |- ( ( ph /\ ( ps /\ ch ) ) -> th )
4	1, 3	mpan 424	1 |- ( ( ps /\ ch ) -> th )

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

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 983

This theorem is referenced by:  mp3an12  1340  mp3an1i  1343  mp3anl1  1344  mp3an  1350  mp3an2i  1355  mp3an3an  1356  tfrlem9  6428  rdgexgg  6487  oaexg  6557  omexg  6560  oeiexg  6562  oav2  6572  nnaordex  6637  mulidnq  7537  1idpru  7739  addgt0sr  7923  muladd11  8240  cnegex  8285  negsubdi  8363  renegcl  8368  mulneg1  8502  ltaddpos  8560  addge01  8580  rimul  8693  recclap  8787  recidap  8794  recidap2  8795  recdivap2  8833  divdiv23apzi  8873  ltmul12a  8968  lemul12a  8970  mulgt1  8971  ltmulgt11  8972  gt0div  8978  ge0div  8979  ltdiv23i  9034  8th4div3  9291  gtndiv  9503  nn0ind  9522  fnn0ind  9524  xrre2  9978  ioorebasg  10132  fzen  10200  elfz0ubfz0  10282  expubnd  10778  le2sq2  10797  bernneq  10842  expnbnd  10845  faclbnd6  10926  bccl  10949  hashfacen  11018  wrdred1hash  11074  ccatlid  11100  swrd0g  11151  shftfval  11247  mulreap  11290  caucvgrelemrec  11405  binom1p  11911  efi4p  12143  sinadd  12162  cosadd  12163  cos2t  12176  cos2tsin  12177  absefib  12197  efieq1re  12198  demoivreALT  12200  odd2np1  12299  opoe  12321  omoe  12322  opeo  12323  omeo  12324  gcdadd  12421  gcdmultiple  12456  algcvgblem  12486  algcvga  12488  isprm3  12555  coprm  12581  1arith2  12806  rmodislmod  14228  cnfldneg  14450  cnfldmulg  14453  cnfldexp  14454  zringmulg  14475  zringsubgval  14482  bl2ioo  15137  ioo2blex  15139  mpomulcn  15153  sinperlem  15395  logge0  15467  lgsdir2  15625  1lgs  15635