Theorem mp3an2 1336

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

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

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 982

This theorem is referenced by:  mp3anl2  1343  ordin  4403  ordsuc  4580  omv  6479  oeiv  6480  omv2  6489  1idprl  7618  muladd11  8119  negsub  8234  subneg  8235  ltaddneg  8410  muleqadd  8654  diveqap1  8691  conjmulap  8715  nnsub  8987  addltmul  9184  zltp1le  9336  gtndiv  9377  eluzp1m1  9580  xnn0le2is012  9895  divelunit  10031  fznatpl1  10105  flqbi2  10321  flqdiv  10351  frecfzen2  10457  nn0ennn  10463  faclbnd3  10754  shftfvalg  10858  ovshftex  10859  shftfval  10861  abs2dif  11146  cos2t  11789  sin01gt0  11800  cos01gt0  11801  demoivre  11811  demoivreALT  11812  omeo  11934  gcd0id  12011  sqgcd  12061  isprm3  12149  eulerthlemth  12263  pczpre  12328  pcrec  12339  setscom  12551  setsslid  12562  setsslnid  12563  mulgm1  13079  abssinper  14719  lgs1  14898