Theorem mp3an2 1261

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

Syntax hints:   -> wi 4   /\ wa 102   /\ w3a 924

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115  df-3an 926

This theorem is referenced by:  mp3anl2  1268  ordin  4210  ordsuc  4377  omv  6208  oeiv  6209  omv2  6218  1idprl  7139  muladd11  7605  negsub  7720  subneg  7721  ltaddneg  7892  muleqadd  8127  diveqap1  8162  conjmulap  8186  nnsub  8451  addltmul  8642  zltp1le  8794  gtndiv  8831  eluzp1m1  9032  divelunit  9409  fznatpl1  9478  flqbi2  9686  flqdiv  9716  frecfzen2  9822  nn0ennn  9828  iseqshft2  9886  faclbnd3  10139  shftfvalg  10240  ovshftex  10241  shftfval  10243  abs2dif  10527  cos2t  11028  sin01gt0  11039  cos01gt0  11040  demoivre  11049  demoivreALT  11050  omeo  11163  gcd0id  11235  sqgcd  11283  isprm3  11365