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  6372  rdgexgg  6431  oaexg  6501  omexg  6504  oeiexg  6506  oav2  6516  nnaordex  6581  mulidnq  7449  1idpru  7651  addgt0sr  7835  muladd11  8152  cnegex  8197  negsubdi  8275  renegcl  8280  mulneg1  8414  ltaddpos  8471  addge01  8491  rimul  8604  recclap  8698  recidap  8705  recidap2  8706  recdivap2  8744  divdiv23apzi  8784  ltmul12a  8879  lemul12a  8881  mulgt1  8882  ltmulgt11  8883  gt0div  8889  ge0div  8890  ltdiv23i  8945  8th4div3  9201  gtndiv  9412  nn0ind  9431  fnn0ind  9433  xrre2  9887  ioorebasg  10041  fzen  10109  elfz0ubfz0  10191  expubnd  10667  le2sq2  10686  bernneq  10731  expnbnd  10734  faclbnd6  10815  bccl  10838  hashfacen  10907  wrdred1hash  10957  shftfval  10965  mulreap  11008  caucvgrelemrec  11123  binom1p  11628  efi4p  11860  sinadd  11879  cosadd  11880  cos2t  11893  cos2tsin  11894  absefib  11914  efieq1re  11915  demoivreALT  11917  odd2np1  12014  opoe  12036  omoe  12037  opeo  12038  omeo  12039  gcdadd  12122  gcdmultiple  12157  algcvgblem  12187  algcvga  12189  isprm3  12256  coprm  12282  1arith2  12506  rmodislmod  13847  cnfldneg  14061  cnfldmulg  14064  cnfldexp  14065  zringmulg  14086  zringsubgval  14093  bl2ioo  14710  ioo2blex  14712  sinperlem  14943  logge0  15015  lgsdir2  15149  1lgs  15159