Theorem mp3an1 1261

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

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

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 927

This theorem is referenced by:  mp3an12  1264  mp3an1i  1267  mp3anl1  1268  mp3an  1274  mp3an2i  1279  mp3an3an  1280  tfrlem9  6100  rdgexgg  6159  oaexg  6225  omexg  6228  oeiexg  6230  oav2  6240  nnaordex  6302  mulidnq  7011  1idpru  7213  addgt0sr  7384  muladd11  7678  cnegex  7723  negsubdi  7801  renegcl  7806  mulneg1  7936  ltaddpos  7993  addge01  8013  rimul  8125  recclap  8209  recidap  8216  recidap2  8217  recdivap2  8255  divdiv23apzi  8295  ltmul12a  8384  lemul12a  8386  mulgt1  8387  ltmulgt11  8388  gt0div  8394  ge0div  8395  ltdiv23i  8450  8th4div3  8698  gtndiv  8904  nn0ind  8923  fnn0ind  8925  xrre2  9346  ioorebasg  9456  fzen  9520  elfz0ubfz0  9599  expubnd  10075  le2sq2  10093  bernneq  10137  expnbnd  10140  faclbnd6  10215  bccl  10238  hashfacen  10304  shftfval  10318  mulreap  10361  caucvgrelemrec  10475  binom1p  10942  efi4p  11071  sinadd  11090  cosadd  11091  cos2t  11104  cos2tsin  11105  absefib  11123  efieq1re  11124  demoivreALT  11126  odd2np1  11214  opoe  11236  omoe  11237  opeo  11238  omeo  11239  gcdadd  11317  gcdmultiple  11350  algcvgblem  11372  algcvga  11374  isprm3  11441  coprm  11464