Theorem mp3an12 1305

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 1302	. 2 |- ( ( ps /\ ch ) -> th )
5	1, 4	mpan 420	1 |- ( ch -> th )

Syntax hints:   -> wi 4   /\ w3a 962

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 964

This theorem is referenced by:  mp3an12i  1319  ceqsralv  2717  brelrn  4772  funpr  5175  fpm  6575  ener  6673  ltaddnq  7215  ltadd1sr  7584  map2psrprg  7613  mul02  8149  ltapi  8398  div0ap  8462  divclapzi  8507  divcanap1zi  8508  divcanap2zi  8509  divrecapzi  8510  divcanap3zi  8511  divcanap4zi  8512  divassapzi  8522  divmulapzi  8523  divdirapzi  8524  redivclapzi  8538  ltm1  8604  mulgt1  8621  recgt1i  8656  recreclt  8658  ltmul1i  8678  ltdiv1i  8679  ltmuldivi  8680  ltmul2i  8681  lemul1i  8682  lemul2i  8683  cju  8719  nnge1  8743  nngt0  8745  nnrecgt0  8758  elnnnn0c  9022  elnnz1  9077  recnz  9144  eluzsubi  9353  ge0gtmnf  9606  m1expcl2  10315  1exp  10322  m1expeven  10340  expubnd  10350  iexpcyc  10397  expnbnd  10415  expnlbnd  10416  remim  10632  imval2  10666  cjdivapi  10707  absdivapzi  10926  ef01bndlem  11463  sin01gt0  11468  cos01gt0  11469  cos12dec  11474  absefib  11477  efieq1re  11478  zeo3  11565  evend2  11586  cnbl0  12703  sincosq1sgn  12907  sincosq3sgn  12909  sincosq4sgn  12910