Theorem mp3an2 1366

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

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

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 1011

This theorem is referenced by:  mp3anl2  1373  ordin  4528  ordsuc  4708  omv  6722  oeiv  6723  omv2  6732  1idprl  7951  muladd11  8453  negsub  8568  subneg  8569  ltaddneg  8746  muleqadd  8992  diveqap1  9029  conjmulap  9053  nnsub  9326  addltmul  9525  zltp1le  9682  gtndiv  9724  eluzp1m1  9929  xnn0le2is012  10251  divelunit  10387  fznatpl1  10466  flqbi2  10709  flqdiv  10741  frecfzen2  10847  nn0ennn  10853  seqshft2g  10902  seqf1oglem1  10939  faclbnd3  11164  ccatrid  11358  shftfvalg  11566  ovshftex  11567  shftfval  11569  abs2dif  11855  cos2t  12500  sin01gt0  12512  cos01gt0  12513  demoivre  12523  demoivreALT  12524  omeo  12648  gcd0id  12739  sqgcd  12789  isprm3  12879  eulerthlemth  12993  pczpre  13059  pcrec  13070  setscom  13375  setsslid  13386  setsslnid  13387  mulgm1  13928  abssinper  15930  lgs1  16146