Theorem mp3an 1268

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

Syntax hints:   -> wi 4   /\ w3a 919

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 921

This theorem is referenced by:  vtocl3  2655  raltp  3449  rextp  3450  ordtriexmidlem  4263  ordtri2or2exmidlem  4269  onsucelsucexmidlem  4272  ordsoexmid  4305  funopg  4954  ftp  5369  caovass  5681  caovdi  5700  ofmres  5783  mpt2fvexi  5852  dmtpos  5894  rntpos  5895  dftpos3  5900  tpostpos  5902  xpcomen  6324  1lt2pi  6530  1lt2nq  6596  halfnqq  6600  m1p1sr  6937  m1m1sr  6938  addassi  7127  mulassi  7128  adddii  7129  adddiri  7130  lttri  7215  lelttri  7216  ltletri  7217  letri  7218  mul12i  7254  mul32i  7255  add12i  7271  add32i  7272  addcani  7290  addcan2i  7291  subaddi  7395  subadd2i  7396  subsub23i  7398  addsubassi  7399  addsubi  7400  subcani  7401  subcan2i  7402  pnncani  7403  subdii  7511  subdiri  7512  ltadd2i  7524  ltadd1i  7603  leadd1i  7604  leadd2i  7605  ltsubaddi  7606  lesubaddi  7607  ltsubadd2i  7608  lesubadd2i  7609  ltaddsubi  7610  gtapii  7732  mulcanapi  7757  divclapi  7842  divcanap2i  7843  divcanap1i  7844  divrecapi  7845  divcanap3i  7846  divcanap4i  7847  divassapi  7856  divdirapi  7857  div23api  7858  div11api  7859  1mhlfehlf  8249  halfpm6th  8251  3halfnz  8444  unirnioo  8996  nnenom  9426  m1expcl2  9498  i4  9577  expnass  9580  bcn1  9685  abs3difi  10042  3dvdsdec  10264  3dvds2dec  10265  ndvdsi  10333  flodddiv4  10334  3lcm2e6woprm  10468  6lcm4e12  10469  3prm  10510  ex-fl  10563