Theorem mp3an1 1314

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

Syntax hints:   -> wi 4   /\ wa 103   /\ w3a 968

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

This theorem depends on definitions:  df-bi 116  df-3an 970

This theorem is referenced by:  mp3an12  1317  mp3an1i  1320  mp3anl1  1321  mp3an  1327  mp3an2i  1332  mp3an3an  1333  tfrlem9  6287  rdgexgg  6346  oaexg  6416  omexg  6419  oeiexg  6421  oav2  6431  nnaordex  6495  mulidnq  7330  1idpru  7532  addgt0sr  7716  muladd11  8031  cnegex  8076  negsubdi  8154  renegcl  8159  mulneg1  8293  ltaddpos  8350  addge01  8370  rimul  8483  recclap  8575  recidap  8582  recidap2  8583  recdivap2  8621  divdiv23apzi  8661  ltmul12a  8755  lemul12a  8757  mulgt1  8758  ltmulgt11  8759  gt0div  8765  ge0div  8766  ltdiv23i  8821  8th4div3  9076  gtndiv  9286  nn0ind  9305  fnn0ind  9307  xrre2  9757  ioorebasg  9911  fzen  9978  elfz0ubfz0  10060  expubnd  10512  le2sq2  10530  bernneq  10575  expnbnd  10578  faclbnd6  10657  bccl  10680  hashfacen  10749  shftfval  10763  mulreap  10806  caucvgrelemrec  10921  binom1p  11426  efi4p  11658  sinadd  11677  cosadd  11678  cos2t  11691  cos2tsin  11692  absefib  11711  efieq1re  11712  demoivreALT  11714  odd2np1  11810  opoe  11832  omoe  11833  opeo  11834  omeo  11835  gcdadd  11918  gcdmultiple  11953  algcvgblem  11981  algcvga  11983  isprm3  12050  coprm  12076  1arith2  12298  bl2ioo  13182  ioo2blex  13184  sinperlem  13369  logge0  13441  lgsdir2  13574  1lgs  13584