Theorem mp3an 1269

Description: An inference based on modus ponens. (Contributed by NM, 14-May-1999.)

Hypotheses

Ref	Expression
mp3an.1	|- ph
mp3an.2	|- ps
mp3an.3	|- ch
mp3an.4	|- ( ( ph /\ ps /\ ch ) -> th )

Assertion

Ref	Expression
mp3an	|- th

Proof of Theorem mp3an

Step	Hyp	Ref	Expression
1		mp3an.2	. 2 |- ps
2		mp3an.3	. 2 |- ch
3		mp3an.1	. . 3 |- ph
4		mp3an.4	. . 3 |- ( ( ph /\ ps /\ ch ) -> th )
5	3, 4	mp3an1 1256	. 2 |- ( ( ps /\ ch ) -> th )
6	1, 2, 5	mp2an 417	1 |- th

Syntax hints:   -> wi 4   /\ w3a 920

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115  df-3an 922

This theorem is referenced by:  vtocl3  2664  raltp  3468  rextp  3469  ordtriexmidlem  4292  ordtri2or2exmidlem  4298  onsucelsucexmidlem  4301  ordsoexmid  4334  funopg  4985  ftp  5401  caovass  5713  caovdi  5732  ofmres  5815  mpt2fvexi  5884  dmtpos  5926  rntpos  5927  dftpos3  5932  tpostpos  5934  xpcomen  6393  unfiexmid  6463  1lt2pi  6628  1lt2nq  6694  halfnqq  6698  m1p1sr  7035  m1m1sr  7036  addassi  7225  mulassi  7226  adddii  7227  adddiri  7228  lttri  7318  lelttri  7319  ltletri  7320  letri  7321  mul12i  7357  mul32i  7358  add12i  7374  add32i  7375  addcani  7393  addcan2i  7394  subaddi  7498  subadd2i  7499  subsub23i  7501  addsubassi  7502  addsubi  7503  subcani  7504  subcan2i  7505  pnncani  7506  subdii  7614  subdiri  7615  ltadd2i  7627  ltadd1i  7706  leadd1i  7707  leadd2i  7708  ltsubaddi  7709  lesubaddi  7710  ltsubadd2i  7711  lesubadd2i  7712  ltaddsubi  7713  gtapii  7835  mulcanapi  7860  divclapi  7945  divcanap2i  7946  divcanap1i  7947  divrecapi  7948  divcanap3i  7949  divcanap4i  7950  divassapi  7959  divdirapi  7960  div23api  7961  div11api  7962  1mhlfehlf  8352  halfpm6th  8354  3halfnz  8561  unirnioo  9108  nnenom  9552  m1expcl2  9631  i4  9710  expnass  9713  bcn1  9818  hashinfom  9838  abs3difi  10227  3dvdsdec  10456  3dvds2dec  10457  ndvdsi  10524  flodddiv4  10525  3lcm2e6woprm  10659  6lcm4e12  10660  3prm  10701  znnen  10802  ex-fl  10807