Theorem mp3an1 1267

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

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

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 929

This theorem is referenced by:  mp3an12  1270  mp3an1i  1273  mp3anl1  1274  mp3an  1280  mp3an2i  1285  mp3an3an  1286  tfrlem9  6122  rdgexgg  6181  oaexg  6249  omexg  6252  oeiexg  6254  oav2  6264  nnaordex  6326  mulidnq  7045  1idpru  7247  addgt0sr  7418  muladd11  7712  cnegex  7757  negsubdi  7835  renegcl  7840  mulneg1  7970  ltaddpos  8027  addge01  8047  rimul  8159  recclap  8243  recidap  8250  recidap2  8251  recdivap2  8289  divdiv23apzi  8329  ltmul12a  8418  lemul12a  8420  mulgt1  8421  ltmulgt11  8422  gt0div  8428  ge0div  8429  ltdiv23i  8484  8th4div3  8733  gtndiv  8940  nn0ind  8959  fnn0ind  8961  xrre2  9387  ioorebasg  9541  fzen  9606  elfz0ubfz0  9685  expubnd  10143  le2sq2  10161  bernneq  10205  expnbnd  10208  faclbnd6  10283  bccl  10306  hashfacen  10372  shftfval  10386  mulreap  10429  caucvgrelemrec  10543  binom1p  11044  efi4p  11173  sinadd  11192  cosadd  11193  cos2t  11206  cos2tsin  11207  absefib  11225  efieq1re  11226  demoivreALT  11228  odd2np1  11316  opoe  11338  omoe  11339  opeo  11340  omeo  11341  gcdadd  11419  gcdmultiple  11452  algcvgblem  11474  algcvga  11476  isprm3  11543  coprm  11566  bl2ioo  12332  ioo2blex  12334