Theorem mp3an2 1359

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

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

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 1004

This theorem is referenced by:  mp3anl2  1366  ordin  4475  ordsuc  4654  omv  6599  oeiv  6600  omv2  6609  1idprl  7773  muladd11  8275  negsub  8390  subneg  8391  ltaddneg  8567  muleqadd  8811  diveqap1  8848  conjmulap  8872  nnsub  9145  addltmul  9344  zltp1le  9497  gtndiv  9538  eluzp1m1  9742  xnn0le2is012  10058  divelunit  10194  fznatpl1  10268  flqbi2  10506  flqdiv  10538  frecfzen2  10644  nn0ennn  10650  seqshft2g  10699  seqf1oglem1  10736  faclbnd3  10960  ccatrid  11137  shftfvalg  11324  ovshftex  11325  shftfval  11327  abs2dif  11612  cos2t  12256  sin01gt0  12268  cos01gt0  12269  demoivre  12279  demoivreALT  12280  omeo  12404  gcd0id  12495  sqgcd  12545  isprm3  12635  eulerthlemth  12749  pczpre  12815  pcrec  12826  setscom  13067  setsslid  13078  setsslnid  13079  mulgm1  13674  abssinper  15514  lgs1  15717