Theorem mp3an1 1358

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

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

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 1004

This theorem is referenced by:  mp3an12  1361  mp3an1i  1364  mp3anl1  1365  mp3an  1371  mp3an2i  1376  mp3an3an  1377  tfrlem9  6480  rdgexgg  6539  oaexg  6611  omexg  6614  oeiexg  6616  oav2  6626  nnaordex  6691  mulidnq  7599  1idpru  7801  addgt0sr  7985  muladd11  8302  cnegex  8347  negsubdi  8425  renegcl  8430  mulneg1  8564  ltaddpos  8622  addge01  8642  rimul  8755  recclap  8849  recidap  8856  recidap2  8857  recdivap2  8895  divdiv23apzi  8935  ltmul12a  9030  lemul12a  9032  mulgt1  9033  ltmulgt11  9034  gt0div  9040  ge0div  9041  ltdiv23i  9096  8th4div3  9353  gtndiv  9565  nn0ind  9584  fnn0ind  9586  xrre2  10046  ioorebasg  10200  fzen  10268  elfz0ubfz0  10350  expubnd  10848  le2sq2  10867  bernneq  10912  expnbnd  10915  faclbnd6  10996  bccl  11019  hashfacen  11090  wrdred1hash  11147  ccatlid  11173  swrd0g  11231  shftfval  11372  mulreap  11415  caucvgrelemrec  11530  binom1p  12036  efi4p  12268  sinadd  12287  cosadd  12288  cos2t  12301  cos2tsin  12302  absefib  12322  efieq1re  12323  demoivreALT  12325  odd2np1  12424  opoe  12446  omoe  12447  opeo  12448  omeo  12449  gcdadd  12546  gcdmultiple  12581  algcvgblem  12611  algcvga  12613  isprm3  12680  coprm  12706  1arith2  12931  rmodislmod  14355  cnfldneg  14577  cnfldmulg  14580  cnfldexp  14581  zringmulg  14602  zringsubgval  14609  bl2ioo  15264  ioo2blex  15266  mpomulcn  15280  sinperlem  15522  logge0  15594  lgsdir2  15752  1lgs  15762