Theorem mp3an 1337

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

Syntax hints:   -> wi 4   /\ w3a 978

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 980

This theorem is referenced by:  vtocl3  2794  raltp  3650  rextp  3651  ordtriexmidlem  4519  ordtri2or2exmidlem  4526  onsucelsucexmidlem  4529  ordsoexmid  4562  funopg  5251  ftp  5702  caovass  6035  caovdi  6054  mptexw  6114  ofmres  6137  mpofvexi  6207  mpoexw  6214  dmtpos  6257  rntpos  6258  dftpos3  6263  tpostpos  6265  mapsnen  6811  xpcomen  6827  mapxpen  6848  xpmapenlem  6849  unfiexmid  6917  1lt2pi  7339  1lt2nq  7405  halfnqq  7409  m1p1sr  7759  m1m1sr  7760  suplocsrlempr  7806  addassi  7965  mulassi  7966  adddii  7967  adddiri  7968  lttri  8062  lelttri  8063  ltletri  8064  letri  8065  mul12i  8103  mul32i  8104  add12i  8120  add32i  8121  addcani  8139  addcan2i  8140  subaddi  8244  subadd2i  8245  subsub23i  8247  addsubassi  8248  addsubi  8249  subcani  8250  subcan2i  8251  pnncani  8252  subdii  8364  subdiri  8365  ltadd2i  8377  ltadd1i  8459  leadd1i  8460  leadd2i  8461  ltsubaddi  8462  lesubaddi  8463  ltsubadd2i  8464  lesubadd2i  8465  ltaddsubi  8466  gtapii  8591  mulcanapi  8624  divclapi  8711  divcanap2i  8712  divcanap1i  8713  divrecapi  8714  divcanap3i  8715  divcanap4i  8716  divassapi  8725  divdirapi  8726  div23api  8727  div11api  8728  sup3exmid  8914  1mhlfehlf  9137  halfpm6th  9139  3halfnz  9350  addex  9651  mulex  9652  unirnioo  9973  nnenom  10434  inftonninf  10441  m1expcl2  10542  i4  10623  expnass  10626  bcn1  10738  hashinfom  10758  abs3difi  11165  0.999...  11529  ef01bndlem  11764  cos1bnd  11767  cos2bnd  11768  sin4lt0  11774  3dvdsdec  11870  3dvds2dec  11871  ndvdsi  11938  flodddiv4  11939  3lcm2e6woprm  12086  6lcm4e12  12087  3prm  12128  znnen  12399  ennnfonelem1  12408  prminf  12456  topnfn  12693  fnmgp  13132  rmodislmodlem  13440  rmodislmod  13441  zring0  13493  xmetunirn  13861  tgioo  14049  tgqioo  14050  addcncntoplem  14054  expcncf  14095  dveflem  14190  dvef  14191  efcn  14192  sinhalfpilem  14215  sincosq1lem  14249  sincosq4sgn  14253  cosq23lt0  14257  coseq00topi  14259  coseq0negpitopi  14260  tangtx  14262  sincos4thpi  14264  sincos6thpi  14266  pigt3  14268  cos02pilt1  14275  cos0pilt1  14276  2logb9irr  14392  2logb3irr  14394  2logb9irrALT  14395  sqrt2cxp2logb9e3  14396  2irrexpq  14397  2logb9irrap  14398  2irrexpqap  14399  lgseisenlem1  14453  lgseisenlem2  14454  ex-fl  14480  ex-exp  14482  trilpolemeq1  14791