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  6552  rdgexgg  6611  oaexg  6683  omexg  6686  oeiexg  6688  oav2  6698  nnaordex  6763  mulidnq  7706  1idpru  7908  addgt0sr  8092  muladd11  8408  cnegex  8453  negsubdi  8531  renegcl  8536  mulneg1  8670  ltaddpos  8728  addge01  8748  rimul  8861  recclap  8955  recidap  8962  recidap2  8963  recdivap2  9001  divdiv23apzi  9041  ltmul12a  9136  lemul12a  9138  mulgt1  9139  ltmulgt11  9140  gt0div  9146  ge0div  9147  ltdiv23i  9202  8th4div3  9459  gtndiv  9676  nn0ind  9695  fnn0ind  9697  xrre2  10157  ioorebasg  10311  fzen  10380  elfz0ubfz0  10463  expubnd  10962  le2sq2  10981  bernneq  11026  expnbnd  11029  faclbnd6  11110  bccl  11133  hashfibc  11211  hashfacen  11212  wrdred1hash  11272  ccatlid  11298  swrd0g  11356  shftfval  11510  mulreap  11553  caucvgrelemrec  11668  binom1p  12175  efi4p  12407  sinadd  12426  cosadd  12427  cos2t  12440  cos2tsin  12441  absefib  12461  efieq1re  12462  demoivreALT  12464  odd2np1  12563  opoe  12585  omoe  12586  opeo  12587  omeo  12588  gcdadd  12685  gcdmultiple  12720  algcvgblem  12750  algcvga  12752  isprm3  12819  coprm  12845  1arith2  13070  ballotfilem2  13149  rmodislmod  14516  cnfldneg  14738  cnfldmulg  14741  cnfldexp  14742  zringmulg  14763  zringsubgval  14770  bl2ioo  15432  ioo2blex  15434  mpomulcn  15448  sinperlem  15690  logge0  15762  lgsdir2  15923  1lgs  15933