Theorem mp3an12 1361

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

Syntax hints:   -> wi 4   /\ 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:  mp3an12i  1375  ceqsralv  2831  brelrn  4957  funpr  5373  fpm  6836  ener  6939  ltaddnq  7605  ltadd1sr  7974  map2psrprg  8003  mul02  8544  ltapi  8794  div0ap  8860  divclapzi  8905  divcanap1zi  8906  divcanap2zi  8907  divrecapzi  8908  divcanap3zi  8909  divcanap4zi  8910  divassapzi  8920  divmulapzi  8921  divdirapzi  8922  redivclapzi  8936  ltm1  9004  mulgt1  9021  recgt1i  9056  recreclt  9058  ltmul1i  9078  ltdiv1i  9079  ltmuldivi  9080  ltmul2i  9081  lemul1i  9082  lemul2i  9083  cju  9119  nnge1  9144  nngt0  9146  nnrecgt0  9159  elnnnn0c  9425  elnnz1  9480  recnz  9551  eluzsubi  9762  ge0gtmnf  10031  m1expcl2  10795  1exp  10802  m1expeven  10820  expubnd  10830  iexpcyc  10878  expnbnd  10897  expnlbnd  10898  remim  11387  imval2  11421  cjdivapi  11462  absdivapzi  11681  fprodge1  12166  ef01bndlem  12283  sin01gt0  12289  cos01gt0  12290  cos12dec  12295  absefib  12298  efieq1re  12299  zeo3  12395  evend2  12416  cnbl0  15224  reeff1olem  15461  sincosq1sgn  15516  sincosq3sgn  15518  sincosq4sgn  15519  rpelogb  15639  lgsdir2lem2  15724