Theorem mp3an1 1324

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

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

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 980

This theorem is referenced by:  mp3an12  1327  mp3an1i  1330  mp3anl1  1331  mp3an  1337  mp3an2i  1342  mp3an3an  1343  tfrlem9  6320  rdgexgg  6379  oaexg  6449  omexg  6452  oeiexg  6454  oav2  6464  nnaordex  6529  mulidnq  7388  1idpru  7590  addgt0sr  7774  muladd11  8090  cnegex  8135  negsubdi  8213  renegcl  8218  mulneg1  8352  ltaddpos  8409  addge01  8429  rimul  8542  recclap  8636  recidap  8643  recidap2  8644  recdivap2  8682  divdiv23apzi  8722  ltmul12a  8817  lemul12a  8819  mulgt1  8820  ltmulgt11  8821  gt0div  8827  ge0div  8828  ltdiv23i  8883  8th4div3  9138  gtndiv  9348  nn0ind  9367  fnn0ind  9369  xrre2  9821  ioorebasg  9975  fzen  10043  elfz0ubfz0  10125  expubnd  10577  le2sq2  10596  bernneq  10641  expnbnd  10644  faclbnd6  10724  bccl  10747  hashfacen  10816  shftfval  10830  mulreap  10873  caucvgrelemrec  10988  binom1p  11493  efi4p  11725  sinadd  11744  cosadd  11745  cos2t  11758  cos2tsin  11759  absefib  11778  efieq1re  11779  demoivreALT  11781  odd2np1  11878  opoe  11900  omoe  11901  opeo  11902  omeo  11903  gcdadd  11986  gcdmultiple  12021  algcvgblem  12049  algcvga  12051  isprm3  12118  coprm  12144  1arith2  12366  rmodislmod  13441  cnfldneg  13470  cnfldmulg  13473  cnfldexp  13474  zringmulg  13491  zringsubgval  13498  bl2ioo  14045  ioo2blex  14047  sinperlem  14232  logge0  14304  lgsdir2  14437  1lgs  14447