Theorem mp3an1 1335

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

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

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 982

This theorem is referenced by:  mp3an12  1338  mp3an1i  1341  mp3anl1  1342  mp3an  1348  mp3an2i  1353  mp3an3an  1354  tfrlem9  6386  rdgexgg  6445  oaexg  6515  omexg  6518  oeiexg  6520  oav2  6530  nnaordex  6595  mulidnq  7475  1idpru  7677  addgt0sr  7861  muladd11  8178  cnegex  8223  negsubdi  8301  renegcl  8306  mulneg1  8440  ltaddpos  8498  addge01  8518  rimul  8631  recclap  8725  recidap  8732  recidap2  8733  recdivap2  8771  divdiv23apzi  8811  ltmul12a  8906  lemul12a  8908  mulgt1  8909  ltmulgt11  8910  gt0div  8916  ge0div  8917  ltdiv23i  8972  8th4div3  9229  gtndiv  9440  nn0ind  9459  fnn0ind  9461  xrre2  9915  ioorebasg  10069  fzen  10137  elfz0ubfz0  10219  expubnd  10707  le2sq2  10726  bernneq  10771  expnbnd  10774  faclbnd6  10855  bccl  10878  hashfacen  10947  wrdred1hash  10997  shftfval  11005  mulreap  11048  caucvgrelemrec  11163  binom1p  11669  efi4p  11901  sinadd  11920  cosadd  11921  cos2t  11934  cos2tsin  11935  absefib  11955  efieq1re  11956  demoivreALT  11958  odd2np1  12057  opoe  12079  omoe  12080  opeo  12081  omeo  12082  gcdadd  12179  gcdmultiple  12214  algcvgblem  12244  algcvga  12246  isprm3  12313  coprm  12339  1arith2  12564  rmodislmod  13985  cnfldneg  14207  cnfldmulg  14210  cnfldexp  14211  zringmulg  14232  zringsubgval  14239  bl2ioo  14894  ioo2blex  14896  mpomulcn  14910  sinperlem  15152  logge0  15224  lgsdir2  15382  1lgs  15392