Theorem mp3an2 1361

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

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

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 1006

This theorem is referenced by:  mp3anl2  1368  ordin  4482  ordsuc  4661  omv  6623  oeiv  6624  omv2  6633  1idprl  7810  muladd11  8312  negsub  8427  subneg  8428  ltaddneg  8604  muleqadd  8848  diveqap1  8885  conjmulap  8909  nnsub  9182  addltmul  9381  zltp1le  9534  gtndiv  9575  eluzp1m1  9780  xnn0le2is012  10101  divelunit  10237  fznatpl1  10311  flqbi2  10552  flqdiv  10584  frecfzen2  10690  nn0ennn  10696  seqshft2g  10745  seqf1oglem1  10782  faclbnd3  11006  ccatrid  11185  shftfvalg  11380  ovshftex  11381  shftfval  11383  abs2dif  11668  cos2t  12313  sin01gt0  12325  cos01gt0  12326  demoivre  12336  demoivreALT  12337  omeo  12461  gcd0id  12552  sqgcd  12602  isprm3  12692  eulerthlemth  12806  pczpre  12872  pcrec  12883  setscom  13124  setsslid  13135  setsslnid  13136  mulgm1  13731  abssinper  15573  lgs1  15776