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 )

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

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 1011

This theorem is referenced by:  mp3an12  1368  mp3an1i  1371  mp3anl1  1372  mp3an  1378  mp3an2i  1383  mp3an3an  1384  tfrlem9  6580  rdgexgg  6639  oaexg  6711  omexg  6714  oeiexg  6716  oav2  6726  nnaordex  6791  mulidnq  7746  1idpru  7948  addgt0sr  8132  muladd11  8449  cnegex  8494  negsubdi  8572  renegcl  8577  mulneg1  8712  ltaddpos  8770  addge01  8790  rimul  8903  recclap  8999  recidap  9006  recidap2  9007  recdivap2  9045  divdiv23apzi  9085  ltmul12a  9180  lemul12a  9182  mulgt1  9183  ltmulgt11  9184  gt0div  9190  ge0div  9191  ltdiv23i  9246  8th4div3  9503  gtndiv  9720  nn0ind  9739  fnn0ind  9741  xrre2  10202  ioorebasg  10356  fzen  10426  elfz0ubfz0  10510  expubnd  11011  le2sq2  11030  bernneq  11076  expnbnd  11079  faclbnd6  11160  bccl  11183  hashfibc  11261  hashfacen  11262  wrdred1hash  11326  ccatlid  11352  swrd0g  11410  shftfval  11564  mulreap  11607  caucvgrelemrec  11723  binom1p  12230  efi4p  12462  sinadd  12481  cosadd  12482  cos2t  12495  cos2tsin  12496  absefib  12516  efieq1re  12517  demoivreALT  12519  odd2np1  12618  opoe  12640  omoe  12641  opeo  12642  omeo  12643  gcdadd  12740  gcdmultiple  12775  algcvgblem  12805  algcvga  12807  isprm3  12874  coprm  12900  1arith2  13125  ballotfilem2  13206  rmodislmod  14660  cnfldneg  14882  cnfldmulg  14885  cnfldexp  14886  zringmulg  14905  zringsubgval  14912  bl2ioo  15574  ioo2blex  15576  mpomulcn  15590  sinperlem  15832  logge0  15904  lgsdir2  16066  1lgs  16076