Theorem mp3an12 1222

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

Syntax hints:   -> wi 4   /\ w3a 885

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110  df-3an 887

This theorem is referenced by:  ceqsralv  2585  brelrn  4567  funpr  4951  ener  6259  ltaddnq  6505  ltadd1sr  6861  mul02  7384  ltapi  7625  div0ap  7679  divclapzi  7723  divcanap1zi  7724  divcanap2zi  7725  divrecapzi  7726  divcanap3zi  7727  divcanap4zi  7728  divassapzi  7738  divmulapzi  7739  divdirapzi  7740  redivclapzi  7754  ltm1  7812  mulgt1  7829  recgt1i  7864  recreclt  7866  ltmul1i  7886  ltdiv1i  7887  ltmuldivi  7888  ltmul2i  7889  lemul1i  7890  lemul2i  7891  cju  7913  nnge1  7937  nngt0  7939  nnrecgt0  7951  elnnnn0c  8227  elnnz1  8268  recnz  8333  eluzsubi  8500  ge0gtmnf  8736  m1expcl2  9277  1exp  9284  expubnd  9311  expnbnd  9372  expnlbnd  9373  remim  9460  imval2  9494  cjdivapi  9535  absdivapzi  9750