Theorem mp3an12 1368

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

This proof depends on syntax axioms:   -> wi 4   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  mp3an12i  1382  ceqsralv  2853  brelrn  5015  funpr  5433  fpm  6962  ener  7066  0fsupp  7298  ltaddnq  7775  ltadd1sr  8144  map2psrprg  8173  mul02  8716  ltapi  8967  div0ap  9035  divclapzi  9080  divcanap1zi  9081  divcanap2zi  9082  divrecapzi  9083  divcanap3zi  9084  divcanap4zi  9085  divassapzi  9095  divmulapzi  9096  divdirapzi  9097  redivclapzi  9111  ltm1  9179  mulgt1  9196  recgt1i  9231  recreclt  9233  ltmul1i  9253  ltdiv1i  9254  ltmuldivi  9255  ltmul2i  9256  lemul1i  9257  lemul2i  9258  cju  9294  nnge1  9330  nngt0  9332  nnrecgt0  9345  elnnnn0c  9613  elnnz1  9672  recnz  9744  eluzsubi  9960  ge0gtmnf  10236  m1expcl2  11013  1exp  11020  m1expeven  11038  expubnd  11048  iexpcyc  11096  resq01  11110  expnbnd  11116  expnlbnd  11117  remim  11641  imval2  11675  cjdivapi  11717  absdivapzi  11937  fprodge1  12425  ef01bndlem  12542  sin01gt0  12548  cos01gt0  12549  cos12dec  12554  absefib  12557  efieq1re  12558  zeo3  12654  evend2  12675  prmlem1  13245  prmlem2  13257  cnbl0  15726  reeff1olem  15963  sincosq1sgn  16019  sincosq3sgn  16021  sincosq4sgn  16022  rpelogb  16146  bposlem8  16279  lgsdir2lem2  16314  konigsberglem5  16899