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  2832  brelrn  4963  funpr  5379  fpm  6845  ener  6948  ltaddnq  7617  ltadd1sr  7986  map2psrprg  8015  mul02  8556  ltapi  8806  div0ap  8872  divclapzi  8917  divcanap1zi  8918  divcanap2zi  8919  divrecapzi  8920  divcanap3zi  8921  divcanap4zi  8922  divassapzi  8932  divmulapzi  8933  divdirapzi  8934  redivclapzi  8948  ltm1  9016  mulgt1  9033  recgt1i  9068  recreclt  9070  ltmul1i  9090  ltdiv1i  9091  ltmuldivi  9092  ltmul2i  9093  lemul1i  9094  lemul2i  9095  cju  9131  nnge1  9156  nngt0  9158  nnrecgt0  9171  elnnnn0c  9437  elnnz1  9492  recnz  9563  eluzsubi  9774  ge0gtmnf  10048  m1expcl2  10813  1exp  10820  m1expeven  10838  expubnd  10848  iexpcyc  10896  expnbnd  10915  expnlbnd  10916  remim  11411  imval2  11445  cjdivapi  11486  absdivapzi  11705  fprodge1  12190  ef01bndlem  12307  sin01gt0  12313  cos01gt0  12314  cos12dec  12319  absefib  12322  efieq1re  12323  zeo3  12419  evend2  12440  cnbl0  15248  reeff1olem  15485  sincosq1sgn  15540  sincosq3sgn  15542  sincosq4sgn  15543  rpelogb  15663  lgsdir2lem2  15748