Theorem mp3an2 1320

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

Syntax hints:   -> wi 4   /\ wa 103   /\ w3a 973

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

This theorem depends on definitions:  df-bi 116  df-3an 975

This theorem is referenced by:  mp3anl2  1327  ordin  4368  ordsuc  4545  omv  6431  oeiv  6432  omv2  6441  1idprl  7539  muladd11  8039  negsub  8154  subneg  8155  ltaddneg  8330  muleqadd  8573  diveqap1  8609  conjmulap  8633  nnsub  8904  addltmul  9101  zltp1le  9253  gtndiv  9294  eluzp1m1  9497  xnn0le2is012  9810  divelunit  9946  fznatpl1  10019  flqbi2  10234  flqdiv  10264  frecfzen2  10370  nn0ennn  10376  faclbnd3  10664  shftfvalg  10769  ovshftex  10770  shftfval  10772  abs2dif  11057  cos2t  11700  sin01gt0  11711  cos01gt0  11712  demoivre  11722  demoivreALT  11723  omeo  11844  gcd0id  11921  sqgcd  11971  isprm3  12059  eulerthlemth  12173  pczpre  12238  pcrec  12249  setscom  12443  setsslid  12453  setsslnid  12454  abssinper  13520  lgs1  13698