Theorem mp3an2 1325

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

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

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 980

This theorem is referenced by:  mp3anl2  1332  ordin  4387  ordsuc  4564  omv  6458  oeiv  6459  omv2  6468  1idprl  7591  muladd11  8092  negsub  8207  subneg  8208  ltaddneg  8383  muleqadd  8627  diveqap1  8664  conjmulap  8688  nnsub  8960  addltmul  9157  zltp1le  9309  gtndiv  9350  eluzp1m1  9553  xnn0le2is012  9868  divelunit  10004  fznatpl1  10078  flqbi2  10293  flqdiv  10323  frecfzen2  10429  nn0ennn  10435  faclbnd3  10725  shftfvalg  10829  ovshftex  10830  shftfval  10832  abs2dif  11117  cos2t  11760  sin01gt0  11771  cos01gt0  11772  demoivre  11782  demoivreALT  11783  omeo  11905  gcd0id  11982  sqgcd  12032  isprm3  12120  eulerthlemth  12234  pczpre  12299  pcrec  12310  setscom  12504  setsslid  12515  setsslnid  12516  mulgm1  13008  abssinper  14306  lgs1  14484