Theorem mp3an12 1338

Description: An inference based on modus ponens. (Contributed by NM, 13-Jul-2005.)

Hypotheses

Ref	Expression
mp3an12.1	|- ph
mp3an12.2	|- ps
mp3an12.3	|- ( ( ph /\ ps /\ ch ) -> th )

Assertion

Ref	Expression
mp3an12	|- ( ch -> th )

Proof of Theorem mp3an12

Step	Hyp	Ref	Expression
1		mp3an12.2	. 2 |- ps
2		mp3an12.1	. . 3 |- ph
3		mp3an12.3	. . 3 |- ( ( ph /\ ps /\ ch ) -> th )
4	2, 3	mp3an1 1335	. 2 |- ( ( ps /\ ch ) -> th )
5	1, 4	mpan 424	1 |- ( ch -> th )

Syntax hints:   -> wi 4   /\ 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:  mp3an12i  1352  ceqsralv  2791  brelrn  4896  funpr  5307  fpm  6737  ener  6835  ltaddnq  7469  ltadd1sr  7838  map2psrprg  7867  mul02  8408  ltapi  8657  div0ap  8723  divclapzi  8768  divcanap1zi  8769  divcanap2zi  8770  divrecapzi  8771  divcanap3zi  8772  divcanap4zi  8773  divassapzi  8783  divmulapzi  8784  divdirapzi  8785  redivclapzi  8799  ltm1  8867  mulgt1  8884  recgt1i  8919  recreclt  8921  ltmul1i  8941  ltdiv1i  8942  ltmuldivi  8943  ltmul2i  8944  lemul1i  8945  lemul2i  8946  cju  8982  nnge1  9007  nngt0  9009  nnrecgt0  9022  elnnnn0c  9288  elnnz1  9343  recnz  9413  eluzsubi  9623  ge0gtmnf  9892  m1expcl2  10635  1exp  10642  m1expeven  10660  expubnd  10670  iexpcyc  10718  expnbnd  10737  expnlbnd  10738  remim  11007  imval2  11041  cjdivapi  11082  absdivapzi  11301  fprodge1  11785  ef01bndlem  11902  sin01gt0  11908  cos01gt0  11909  cos12dec  11914  absefib  11917  efieq1re  11918  zeo3  12012  evend2  12033  cnbl0  14713  reeff1olem  14947  sincosq1sgn  15002  sincosq3sgn  15004  sincosq4sgn  15005  rpelogb  15122  lgsdir2lem2  15186