Theorem mp3an 1374

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

Syntax hints:   -> wi 4   /\ w3a 1005

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 1007

This theorem is referenced by:  vtocl3  2873  raltp  3751  rextp  3752  ordtriexmidlem  4646  ordtri2or2exmidlem  4653  onsucelsucexmidlem  4656  ordsoexmid  4689  funopg  5391  ftp  5874  caovass  6223  caovdi  6242  mptexw  6315  ofmres  6342  mpofvexi  6415  mpoexw  6422  dmtpos  6500  rntpos  6501  dftpos3  6506  tpostpos  6508  mapsnen  7066  xpcomen  7091  mapxpen  7114  xpmapenlem  7115  unfiexmid  7191  1lt2pi  7671  1lt2nq  7737  halfnqq  7741  m1p1sr  8091  m1m1sr  8092  suplocsrlempr  8138  addassi  8298  mulassi  8299  adddii  8300  adddiri  8301  lttri  8394  lelttri  8395  ltletri  8396  letri  8397  mul12i  8435  mul32i  8436  add12i  8452  add32i  8453  addcani  8471  addcan2i  8472  subaddi  8576  subadd2i  8577  subsub23i  8579  addsubassi  8580  addsubi  8581  subcani  8582  subcan2i  8583  pnncani  8584  subdii  8697  subdiri  8698  ltadd2i  8711  ltadd1i  8793  leadd1i  8794  leadd2i  8795  ltsubaddi  8796  lesubaddi  8797  ltsubadd2i  8798  lesubadd2i  8799  ltaddsubi  8800  gtapii  8925  mulcanapi  8958  divclapi  9045  divcanap2i  9046  divcanap1i  9047  divrecapi  9048  divcanap3i  9049  divcanap4i  9050  divassapi  9059  divdirapi  9060  div23api  9061  div11api  9062  sup3exmid  9248  1mhlfehlf  9473  halfpm6th  9475  3halfnz  9693  addex  10002  mulex  10003  unirnioo  10325  nnenom  10820  inftonninf  10828  m1expcl2  10947  i4  11028  expnass  11031  bcn1  11145  hashinfom  11166  abs3difi  11866  0.999...  12232  ef01bndlem  12467  cos1bnd  12470  cos2bnd  12471  sin4lt0  12478  3dvdsdec  12576  3dvds2dec  12577  ndvdsi  12644  flodddiv4  12647  3lcm2e6woprm  12808  6lcm4e12  12809  3prm  12850  dec2dvds  13134  modxai  13139  gcdi  13143  numexp2x  13148  2exp5  13155  2exp11  13159  ballotfilem2  13172  ballotfilemafi  13182  ballotfilembfi  13183  ballotfilem4  13185  ballotfilemi1  13189  ballotfilemth  13225  znnen  13233  ennnfonelem1  13242  prminf  13290  topnfn  13541  prdsvallem  13564  prdsval  14115  fnmgp  14161  rhmex  14402  rmodislmodlem  14624  rmodislmod  14625  cnfldstr  14832  zring0  14874  fnpsr  14941  mplvalcoe  14971  fnmpl  14974  xmetunirn  15349  tgioo  15545  tgqioo  15546  addcncntoplem  15552  expcncf  15600  dveflem  15717  dvef  15718  efcn  15759  sinhalfpilem  15782  sincosq1lem  15816  sincosq4sgn  15820  cosq23lt0  15824  coseq00topi  15826  coseq0negpitopi  15827  tangtx  15829  sincos4thpi  15831  sincos6thpi  15833  pigt3  15835  cos02pilt1  15842  cos0pilt1  15843  2logb9irr  15962  2logb3irr  15964  2logb9irrALT  15965  sqrt2cxp2logb9e3  15966  2irrexpq  15967  2logb9irrap  15968  2irrexpqap  15969  1sgm2ppw  15989  lgseisenlem1  16069  lgseisenlem2  16070  lgsquadlem1  16076  upgr2wlkdc  16498  konigsberglem1  16609  konigsberglem2  16610  konigsberglem3  16611  konigsberglem5  16613  ex-fl  16619  ex-exp  16621  repiecelem  16935  repiecege0  16937  trilpolemeq1  16950