Theorem mp3an 1232

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 1219	. 2 |- ( ( ps /\ ch ) -> th )
6	1, 2, 5	mp2an 402	1 |- 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:  vtocl3  2610  raltp  3427  rextp  3428  ordtriexmidlem  4245  ordtri2or2exmidlem  4251  onsucelsucexmidlem  4254  ordsoexmid  4286  funopg  4934  ftp  5348  caovass  5661  caovdi  5680  ofmres  5763  mpt2fvexi  5832  dmtpos  5871  rntpos  5872  dftpos3  5877  tpostpos  5879  xpcomen  6301  1lt2pi  6438  1lt2nq  6504  halfnqq  6508  m1p1sr  6845  m1m1sr  6846  addassi  7035  mulassi  7036  adddii  7037  adddiri  7038  lttri  7122  lelttri  7123  ltletri  7124  letri  7125  mul12i  7159  mul32i  7160  add12i  7174  add32i  7175  addcani  7193  addcan2i  7194  subaddi  7298  subadd2i  7299  subsub23i  7301  addsubassi  7302  addsubi  7303  subcani  7304  subcan2i  7305  pnncani  7306  subdii  7404  subdiri  7405  ltadd2i  7417  ltadd1i  7494  leadd1i  7495  leadd2i  7496  ltsubaddi  7497  lesubaddi  7498  ltsubadd2i  7499  lesubadd2i  7500  ltaddsubi  7501  gtapii  7623  mulcanapi  7648  divclapi  7730  divcanap2i  7731  divcanap1i  7732  divrecapi  7733  divcanap3i  7734  divcanap4i  7735  divassapi  7744  divdirapi  7745  div23api  7746  div11api  7747  1mhlfehlf  8143  halfpm6th  8145  unirnioo  8842  nnenom  9210  m1expcl2  9277  i4  9355  expnass  9357  abs3difi  9752  ex-fl  9895