Theorem mp3an1 1306

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

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

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 965

This theorem is referenced by:  mp3an12  1309  mp3an1i  1312  mp3anl1  1313  mp3an  1319  mp3an2i  1324  mp3an3an  1325  tfrlem9  6266  rdgexgg  6325  oaexg  6395  omexg  6398  oeiexg  6400  oav2  6410  nnaordex  6474  mulidnq  7309  1idpru  7511  addgt0sr  7695  muladd11  8008  cnegex  8053  negsubdi  8131  renegcl  8136  mulneg1  8270  ltaddpos  8327  addge01  8347  rimul  8460  recclap  8552  recidap  8559  recidap2  8560  recdivap2  8598  divdiv23apzi  8638  ltmul12a  8731  lemul12a  8733  mulgt1  8734  ltmulgt11  8735  gt0div  8741  ge0div  8742  ltdiv23i  8797  8th4div3  9052  gtndiv  9259  nn0ind  9278  fnn0ind  9280  xrre2  9725  ioorebasg  9879  fzen  9945  elfz0ubfz0  10024  expubnd  10476  le2sq2  10494  bernneq  10538  expnbnd  10541  faclbnd6  10618  bccl  10641  hashfacen  10707  shftfval  10721  mulreap  10764  caucvgrelemrec  10879  binom1p  11382  efi4p  11614  sinadd  11633  cosadd  11634  cos2t  11647  cos2tsin  11648  absefib  11667  efieq1re  11668  demoivreALT  11670  odd2np1  11763  opoe  11785  omoe  11786  opeo  11787  omeo  11788  gcdadd  11868  gcdmultiple  11903  algcvgblem  11925  algcvga  11927  isprm3  11994  coprm  12018  bl2ioo  12942  ioo2blex  12944  sinperlem  13129  logge0  13201