Theorem mp3an1 1365

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  mp3an12  1368  mp3an1i  1371  mp3anl1  1372  mp3an  1378  mp3an2i  1383  mp3an3an  1384  tfrlem9  6595  rdgexgg  6654  oaexg  6726  omexg  6729  oeiexg  6731  oav2  6741  nnaordex  6806  mulidnq  7762  1idpru  7964  addgt0sr  8148  muladd11  8466  cnegex  8511  negsubdi  8589  renegcl  8594  mulneg1  8729  ltaddpos  8787  addge01  8807  rimul  8921  recclap  9017  recidap  9024  recidap2  9025  recdivap2  9063  divdiv23apzi  9103  ltmul12a  9198  lemul12a  9200  mulgt1  9201  ltmulgt11  9202  gt0div  9208  ge0div  9209  ltdiv23i  9264  8th4div3  9535  gtndiv  9751  nn0ind  9770  fnn0ind  9772  xrre2  10239  ioorebasg  10393  fzen  10463  elfz0ubfz0  10548  expubnd  11053  le2sq2  11072  bernneq  11118  expnbnd  11121  faclbnd6  11203  bccl  11226  hashfibc  11304  hashfacen  11305  wrdred1hash  11369  ccatlid  11395  swrd0g  11453  shftfval  11607  mulreap  11650  caucvgrelemrec  11766  binom1p  12276  efi4p  12508  sinadd  12527  cosadd  12528  cos2t  12541  cos2tsin  12542  absefib  12562  efieq1re  12563  demoivreALT  12565  odd2np1  12664  opoe  12686  omoe  12687  opeo  12688  omeo  12689  gcdadd  12786  gcdmultiple  12821  algcvgblem  12851  algcvga  12853  isprm3  12920  coprm  12947  1arith2  13175  ballotfilem2  13285  rmodislmod  14796  cnfldneg  15018  cnfldmulg  15021  cnfldexp  15022  zringmulg  15041  zringsubgval  15048  mplbas  15223  bl2ioo  15793  ioo2blex  15795  mpomulcn  15809  sinperlem  16052  logge0  16127  ppiqnncl  16295  chtqrpcl  16296  bposlem2  16329  bposlem8  16335  lgsdir2  16374  1lgs  16384