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  4370  ordsuc  4547  omv  6434  oeiv  6435  omv2  6444  1idprl  7552  muladd11  8052  negsub  8167  subneg  8168  ltaddneg  8343  muleqadd  8586  diveqap1  8622  conjmulap  8646  nnsub  8917  addltmul  9114  zltp1le  9266  gtndiv  9307  eluzp1m1  9510  xnn0le2is012  9823  divelunit  9959  fznatpl1  10032  flqbi2  10247  flqdiv  10277  frecfzen2  10383  nn0ennn  10389  faclbnd3  10677  shftfvalg  10782  ovshftex  10783  shftfval  10785  abs2dif  11070  cos2t  11713  sin01gt0  11724  cos01gt0  11725  demoivre  11735  demoivreALT  11736  omeo  11857  gcd0id  11934  sqgcd  11984  isprm3  12072  eulerthlemth  12186  pczpre  12251  pcrec  12262  setscom  12456  setsslid  12466  setsslnid  12467  abssinper  13561  lgs1  13739