Theorem mp3an2 1336

Description: An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.)

Hypotheses

Ref	Expression
mp3an2.1	|- ps
mp3an2.2	|- ( ( ph /\ ps /\ ch ) -> th )

Assertion

Ref	Expression
mp3an2	|- ( ( ph /\ ch ) -> th )

Proof of Theorem mp3an2

Step	Hyp	Ref	Expression
1		mp3an2.1	. 2 |- ps
2		mp3an2.2	. . 3 |- ( ( ph /\ ps /\ ch ) -> th )
3	2	3expa 1205	. 2 |- ( ( ( ph /\ ps ) /\ ch ) -> th )
4	1, 3	mpanl2 435	1 |- ( ( ph /\ 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:  mp3anl2  1343  ordin  4420  ordsuc  4599  omv  6513  oeiv  6514  omv2  6523  1idprl  7657  muladd11  8159  negsub  8274  subneg  8275  ltaddneg  8451  muleqadd  8695  diveqap1  8732  conjmulap  8756  nnsub  9029  addltmul  9228  zltp1le  9380  gtndiv  9421  eluzp1m1  9625  xnn0le2is012  9941  divelunit  10077  fznatpl1  10151  flqbi2  10381  flqdiv  10413  frecfzen2  10519  nn0ennn  10525  seqshft2g  10574  seqf1oglem1  10611  faclbnd3  10835  shftfvalg  10983  ovshftex  10984  shftfval  10986  abs2dif  11271  cos2t  11915  sin01gt0  11927  cos01gt0  11928  demoivre  11938  demoivreALT  11939  omeo  12063  gcd0id  12146  sqgcd  12196  isprm3  12286  eulerthlemth  12400  pczpre  12466  pcrec  12477  setscom  12718  setsslid  12729  setsslnid  12730  mulgm1  13272  abssinper  15082  lgs1  15285