Theorem mp3an2 1361

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

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

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 1006

This theorem is referenced by:  mp3anl2  1368  ordin  4484  ordsuc  4663  omv  6628  oeiv  6629  omv2  6638  1idprl  7815  muladd11  8317  negsub  8432  subneg  8433  ltaddneg  8609  muleqadd  8853  diveqap1  8890  conjmulap  8914  nnsub  9187  addltmul  9386  zltp1le  9539  gtndiv  9580  eluzp1m1  9785  xnn0le2is012  10106  divelunit  10242  fznatpl1  10316  flqbi2  10557  flqdiv  10589  frecfzen2  10695  nn0ennn  10701  seqshft2g  10750  seqf1oglem1  10787  faclbnd3  11011  ccatrid  11193  shftfvalg  11401  ovshftex  11402  shftfval  11404  abs2dif  11689  cos2t  12334  sin01gt0  12346  cos01gt0  12347  demoivre  12357  demoivreALT  12358  omeo  12482  gcd0id  12573  sqgcd  12623  isprm3  12713  eulerthlemth  12827  pczpre  12893  pcrec  12904  setscom  13145  setsslid  13156  setsslnid  13157  mulgm1  13752  abssinper  15599  lgs1  15802