Theorem mp3an2 1340

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

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

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 985

This theorem is referenced by:  mp3anl2  1347  ordin  4453  ordsuc  4632  omv  6571  oeiv  6572  omv2  6581  1idprl  7745  muladd11  8247  negsub  8362  subneg  8363  ltaddneg  8539  muleqadd  8783  diveqap1  8820  conjmulap  8844  nnsub  9117  addltmul  9316  zltp1le  9469  gtndiv  9510  eluzp1m1  9714  xnn0le2is012  10030  divelunit  10166  fznatpl1  10240  flqbi2  10478  flqdiv  10510  frecfzen2  10616  nn0ennn  10622  seqshft2g  10671  seqf1oglem1  10708  faclbnd3  10932  ccatrid  11108  shftfvalg  11295  ovshftex  11296  shftfval  11298  abs2dif  11583  cos2t  12227  sin01gt0  12239  cos01gt0  12240  demoivre  12250  demoivreALT  12251  omeo  12375  gcd0id  12466  sqgcd  12516  isprm3  12606  eulerthlemth  12720  pczpre  12786  pcrec  12797  setscom  13038  setsslid  13049  setsslnid  13050  mulgm1  13645  abssinper  15485  lgs1  15688