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  4477  ordsuc  4656  omv  6614  oeiv  6615  omv2  6624  1idprl  7793  muladd11  8295  negsub  8410  subneg  8411  ltaddneg  8587  muleqadd  8831  diveqap1  8868  conjmulap  8892  nnsub  9165  addltmul  9364  zltp1le  9517  gtndiv  9558  eluzp1m1  9763  xnn0le2is012  10079  divelunit  10215  fznatpl1  10289  flqbi2  10528  flqdiv  10560  frecfzen2  10666  nn0ennn  10672  seqshft2g  10721  seqf1oglem1  10758  faclbnd3  10982  ccatrid  11160  shftfvalg  11350  ovshftex  11351  shftfval  11353  abs2dif  11638  cos2t  12282  sin01gt0  12294  cos01gt0  12295  demoivre  12305  demoivreALT  12306  omeo  12430  gcd0id  12521  sqgcd  12571  isprm3  12661  eulerthlemth  12775  pczpre  12841  pcrec  12852  setscom  13093  setsslid  13104  setsslnid  13105  mulgm1  13700  abssinper  15541  lgs1  15744