Theorem mp3an 1243

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 1230	. 2 |- ( ( ps /\ ch ) -> th )
6	1, 2, 5	mp2an 410	1 |- th

Syntax hints:   -> wi 4   /\ w3a 896

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

This theorem depends on definitions:  df-bi 114  df-3an 898

This theorem is referenced by:  vtocl3  2627  raltp  3454  rextp  3455  ordtriexmidlem  4272  ordtri2or2exmidlem  4278  onsucelsucexmidlem  4281  ordsoexmid  4313  funopg  4961  ftp  5375  caovass  5688  caovdi  5707  ofmres  5790  mpt2fvexi  5859  dmtpos  5901  rntpos  5902  dftpos3  5907  tpostpos  5909  xpcomen  6331  1lt2pi  6495  1lt2nq  6561  halfnqq  6565  m1p1sr  6902  m1m1sr  6903  addassi  7092  mulassi  7093  adddii  7094  adddiri  7095  lttri  7180  lelttri  7181  ltletri  7182  letri  7183  mul12i  7219  mul32i  7220  add12i  7236  add32i  7237  addcani  7255  addcan2i  7256  subaddi  7360  subadd2i  7361  subsub23i  7363  addsubassi  7364  addsubi  7365  subcani  7366  subcan2i  7367  pnncani  7368  subdii  7475  subdiri  7476  ltadd2i  7488  ltadd1i  7567  leadd1i  7568  leadd2i  7569  ltsubaddi  7570  lesubaddi  7571  ltsubadd2i  7572  lesubadd2i  7573  ltaddsubi  7574  gtapii  7696  mulcanapi  7721  divclapi  7804  divcanap2i  7805  divcanap1i  7806  divrecapi  7807  divcanap3i  7808  divcanap4i  7809  divassapi  7818  divdirapi  7819  div23api  7820  div11api  7821  1mhlfehlf  8199  halfpm6th  8201  3halfnz  8394  unirnioo  8942  nnenom  9368  m1expcl2  9436  i4  9515  expnass  9517  bcn1  9619  abs3difi  9975  3dvdsdec  10168  3dvds2dec  10169  ex-fl  10251