Theorem mp3an1 1319

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

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

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 975

This theorem is referenced by:  mp3an12  1322  mp3an1i  1325  mp3anl1  1326  mp3an  1332  mp3an2i  1337  mp3an3an  1338  tfrlem9  6298  rdgexgg  6357  oaexg  6427  omexg  6430  oeiexg  6432  oav2  6442  nnaordex  6507  mulidnq  7351  1idpru  7553  addgt0sr  7737  muladd11  8052  cnegex  8097  negsubdi  8175  renegcl  8180  mulneg1  8314  ltaddpos  8371  addge01  8391  rimul  8504  recclap  8596  recidap  8603  recidap2  8604  recdivap2  8642  divdiv23apzi  8682  ltmul12a  8776  lemul12a  8778  mulgt1  8779  ltmulgt11  8780  gt0div  8786  ge0div  8787  ltdiv23i  8842  8th4div3  9097  gtndiv  9307  nn0ind  9326  fnn0ind  9328  xrre2  9778  ioorebasg  9932  fzen  9999  elfz0ubfz0  10081  expubnd  10533  le2sq2  10551  bernneq  10596  expnbnd  10599  faclbnd6  10678  bccl  10701  hashfacen  10771  shftfval  10785  mulreap  10828  caucvgrelemrec  10943  binom1p  11448  efi4p  11680  sinadd  11699  cosadd  11700  cos2t  11713  cos2tsin  11714  absefib  11733  efieq1re  11734  demoivreALT  11736  odd2np1  11832  opoe  11854  omoe  11855  opeo  11856  omeo  11857  gcdadd  11940  gcdmultiple  11975  algcvgblem  12003  algcvga  12005  isprm3  12072  coprm  12098  1arith2  12320  bl2ioo  13336  ioo2blex  13338  sinperlem  13523  logge0  13595  lgsdir2  13728  1lgs  13738