Theorem mp3an12 1316

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

Syntax hints:   -> wi 4   /\ w3a 967

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 969

This theorem is referenced by:  mp3an12i  1330  ceqsralv  2752  brelrn  4831  funpr  5234  fpm  6638  ener  6736  ltaddnq  7339  ltadd1sr  7708  map2psrprg  7737  mul02  8276  ltapi  8525  div0ap  8589  divclapzi  8634  divcanap1zi  8635  divcanap2zi  8636  divrecapzi  8637  divcanap3zi  8638  divcanap4zi  8639  divassapzi  8649  divmulapzi  8650  divdirapzi  8651  redivclapzi  8665  ltm1  8732  mulgt1  8749  recgt1i  8784  recreclt  8786  ltmul1i  8806  ltdiv1i  8807  ltmuldivi  8808  ltmul2i  8809  lemul1i  8810  lemul2i  8811  cju  8847  nnge1  8871  nngt0  8873  nnrecgt0  8886  elnnnn0c  9150  elnnz1  9205  recnz  9275  eluzsubi  9484  ge0gtmnf  9750  m1expcl2  10467  1exp  10474  m1expeven  10492  expubnd  10502  iexpcyc  10549  expnbnd  10567  expnlbnd  10568  remim  10788  imval2  10822  cjdivapi  10863  absdivapzi  11082  fprodge1  11566  ef01bndlem  11683  sin01gt0  11688  cos01gt0  11689  cos12dec  11694  absefib  11697  efieq1re  11698  zeo3  11790  evend2  11811  cnbl0  13075  reeff1olem  13233  sincosq1sgn  13288  sincosq3sgn  13290  sincosq4sgn  13291  rpelogb  13408