Theorem mp3an2 1315

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

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

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 970

This theorem is referenced by:  mp3anl2  1322  ordin  4362  ordsuc  4539  omv  6419  oeiv  6420  omv2  6429  1idprl  7527  muladd11  8027  negsub  8142  subneg  8143  ltaddneg  8318  muleqadd  8561  diveqap1  8597  conjmulap  8621  nnsub  8892  addltmul  9089  zltp1le  9241  gtndiv  9282  eluzp1m1  9485  xnn0le2is012  9798  divelunit  9934  fznatpl1  10007  flqbi2  10222  flqdiv  10252  frecfzen2  10358  nn0ennn  10364  faclbnd3  10652  shftfvalg  10756  ovshftex  10757  shftfval  10759  abs2dif  11044  cos2t  11687  sin01gt0  11698  cos01gt0  11699  demoivre  11709  demoivreALT  11710  omeo  11831  gcd0id  11908  sqgcd  11958  isprm3  12046  eulerthlemth  12160  pczpre  12225  pcrec  12236  setscom  12430  setsslid  12440  setsslnid  12441  abssinper  13367  lgs1  13545