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  7473  1idpru  7675  addgt0sr  7859  muladd11  8176  cnegex  8221  negsubdi  8299  renegcl  8304  mulneg1  8438  ltaddpos  8496  addge01  8516  rimul  8629  recclap  8723  recidap  8730  recidap2  8731  recdivap2  8769  divdiv23apzi  8809  ltmul12a  8904  lemul12a  8906  mulgt1  8907  ltmulgt11  8908  gt0div  8914  ge0div  8915  ltdiv23i  8970  8th4div3  9227  gtndiv  9438  nn0ind  9457  fnn0ind  9459  xrre2  9913  ioorebasg  10067  fzen  10135  elfz0ubfz0  10217  expubnd  10705  le2sq2  10724  bernneq  10769  expnbnd  10772  faclbnd6  10853  bccl  10876  hashfacen  10945  wrdred1hash  10995  shftfval  11003  mulreap  11046  caucvgrelemrec  11161  binom1p  11667  efi4p  11899  sinadd  11918  cosadd  11919  cos2t  11932  cos2tsin  11933  absefib  11953  efieq1re  11954  demoivreALT  11956  odd2np1  12055  opoe  12077  omoe  12078  opeo  12079  omeo  12080  gcdadd  12177  gcdmultiple  12212  algcvgblem  12242  algcvga  12244  isprm3  12311  coprm  12337  1arith2  12562  rmodislmod  13983  cnfldneg  14205  cnfldmulg  14208  cnfldexp  14209  zringmulg  14230  zringsubgval  14237  bl2ioo  14870  ioo2blex  14872  mpomulcn  14886  sinperlem  15128  logge0  15200  lgsdir2  15358  1lgs  15368