Theorem mp3an2 1362

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 1230	. 2 |- ( ( ( ph /\ ps ) /\ ch ) -> th )
4	1, 3	mpanl2 435	1 |- ( ( ph /\ ch ) -> th )

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 1005

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 1007

This theorem is referenced by:  mp3anl2  1369  ordin  4508  ordsuc  4687  omv  6690  oeiv  6691  omv2  6700  1idprl  7910  muladd11  8411  negsub  8526  subneg  8527  ltaddneg  8703  muleqadd  8947  diveqap1  8984  conjmulap  9008  nnsub  9281  addltmul  9480  zltp1le  9637  gtndiv  9679  eluzp1m1  9884  xnn0le2is012  10205  divelunit  10341  fznatpl1  10417  flqbi2  10658  flqdiv  10690  frecfzen2  10796  nn0ennn  10802  seqshft2g  10851  seqf1oglem1  10888  faclbnd3  11113  ccatrid  11303  shftfvalg  11511  ovshftex  11512  shftfval  11514  abs2dif  11799  cos2t  12444  sin01gt0  12456  cos01gt0  12457  demoivre  12467  demoivreALT  12468  omeo  12592  gcd0id  12683  sqgcd  12733  isprm3  12823  eulerthlemth  12937  pczpre  13003  pcrec  13014  setscom  13273  setsslid  13284  setsslnid  13285  mulgm1  13880  abssinper  15760  lgs1  15966