Theorem mp3an1 1361

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

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

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 1007

This theorem is referenced by:  mp3an12  1364  mp3an1i  1367  mp3anl1  1368  mp3an  1374  mp3an2i  1379  mp3an3an  1380  tfrlem9  6563  rdgexgg  6622  oaexg  6694  omexg  6697  oeiexg  6699  oav2  6709  nnaordex  6774  mulidnq  7720  1idpru  7922  addgt0sr  8106  muladd11  8422  cnegex  8467  negsubdi  8545  renegcl  8550  mulneg1  8685  ltaddpos  8743  addge01  8763  rimul  8876  recclap  8970  recidap  8977  recidap2  8978  recdivap2  9016  divdiv23apzi  9056  ltmul12a  9151  lemul12a  9153  mulgt1  9154  ltmulgt11  9155  gt0div  9161  ge0div  9162  ltdiv23i  9217  8th4div3  9474  gtndiv  9691  nn0ind  9710  fnn0ind  9712  xrre2  10173  ioorebasg  10327  fzen  10397  elfz0ubfz0  10481  expubnd  10982  le2sq2  11001  bernneq  11047  expnbnd  11050  faclbnd6  11131  bccl  11154  hashfibc  11232  hashfacen  11233  wrdred1hash  11293  ccatlid  11319  swrd0g  11377  shftfval  11531  mulreap  11574  caucvgrelemrec  11689  binom1p  12196  efi4p  12428  sinadd  12447  cosadd  12448  cos2t  12461  cos2tsin  12462  absefib  12482  efieq1re  12483  demoivreALT  12485  odd2np1  12584  opoe  12606  omoe  12607  opeo  12608  omeo  12609  gcdadd  12706  gcdmultiple  12741  algcvgblem  12771  algcvga  12773  isprm3  12840  coprm  12866  1arith2  13091  ballotfilem2  13172  rmodislmod  14625  cnfldneg  14847  cnfldmulg  14850  cnfldexp  14851  zringmulg  14872  zringsubgval  14879  bl2ioo  15541  ioo2blex  15543  mpomulcn  15557  sinperlem  15799  logge0  15871  lgsdir2  16032  1lgs  16042