Theorem mp3an12 1317

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

Syntax hints:   -> wi 4   /\ w3a 968

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 970

This theorem is referenced by:  mp3an12i  1331  ceqsralv  2757  brelrn  4837  funpr  5240  fpm  6647  ener  6745  ltaddnq  7348  ltadd1sr  7717  map2psrprg  7746  mul02  8285  ltapi  8534  div0ap  8598  divclapzi  8643  divcanap1zi  8644  divcanap2zi  8645  divrecapzi  8646  divcanap3zi  8647  divcanap4zi  8648  divassapzi  8658  divmulapzi  8659  divdirapzi  8660  redivclapzi  8674  ltm1  8741  mulgt1  8758  recgt1i  8793  recreclt  8795  ltmul1i  8815  ltdiv1i  8816  ltmuldivi  8817  ltmul2i  8818  lemul1i  8819  lemul2i  8820  cju  8856  nnge1  8880  nngt0  8882  nnrecgt0  8895  elnnnn0c  9159  elnnz1  9214  recnz  9284  eluzsubi  9493  ge0gtmnf  9759  m1expcl2  10477  1exp  10484  m1expeven  10502  expubnd  10512  iexpcyc  10559  expnbnd  10578  expnlbnd  10579  remim  10802  imval2  10836  cjdivapi  10877  absdivapzi  11096  fprodge1  11580  ef01bndlem  11697  sin01gt0  11702  cos01gt0  11703  cos12dec  11708  absefib  11711  efieq1re  11712  zeo3  11805  evend2  11826  cnbl0  13174  reeff1olem  13332  sincosq1sgn  13387  sincosq3sgn  13389  sincosq4sgn  13390  rpelogb  13507  lgsdir2lem2  13570