Theorem mp3an 1350

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

Syntax hints:   -> wi 4   /\ w3a 981

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 983

This theorem is referenced by:  vtocl3  2834  raltp  3700  rextp  3701  ordtriexmidlem  4585  ordtri2or2exmidlem  4592  onsucelsucexmidlem  4595  ordsoexmid  4628  funopg  5324  ftp  5792  caovass  6130  caovdi  6149  mptexw  6221  ofmres  6244  mpofvexi  6315  mpoexw  6322  dmtpos  6365  rntpos  6366  dftpos3  6371  tpostpos  6373  mapsnen  6927  xpcomen  6947  mapxpen  6970  xpmapenlem  6971  unfiexmid  7041  1lt2pi  7488  1lt2nq  7554  halfnqq  7558  m1p1sr  7908  m1m1sr  7909  suplocsrlempr  7955  addassi  8115  mulassi  8116  adddii  8117  adddiri  8118  lttri  8212  lelttri  8213  ltletri  8214  letri  8215  mul12i  8253  mul32i  8254  add12i  8270  add32i  8271  addcani  8289  addcan2i  8290  subaddi  8394  subadd2i  8395  subsub23i  8397  addsubassi  8398  addsubi  8399  subcani  8400  subcan2i  8401  pnncani  8402  subdii  8514  subdiri  8515  ltadd2i  8528  ltadd1i  8610  leadd1i  8611  leadd2i  8612  ltsubaddi  8613  lesubaddi  8614  ltsubadd2i  8615  lesubadd2i  8616  ltaddsubi  8617  gtapii  8742  mulcanapi  8775  divclapi  8862  divcanap2i  8863  divcanap1i  8864  divrecapi  8865  divcanap3i  8866  divcanap4i  8867  divassapi  8876  divdirapi  8877  div23api  8878  div11api  8879  sup3exmid  9065  1mhlfehlf  9290  halfpm6th  9292  3halfnz  9505  addex  9808  mulex  9809  unirnioo  10130  nnenom  10616  inftonninf  10624  m1expcl2  10743  i4  10824  expnass  10827  bcn1  10940  hashinfom  10960  abs3difi  11582  0.999...  11947  ef01bndlem  12182  cos1bnd  12185  cos2bnd  12186  sin4lt0  12193  3dvdsdec  12291  3dvds2dec  12292  ndvdsi  12359  flodddiv4  12362  3lcm2e6woprm  12523  6lcm4e12  12524  3prm  12565  dec2dvds  12849  modxai  12854  gcdi  12858  numexp2x  12863  2exp5  12870  2exp11  12874  znnen  12884  ennnfonelem1  12893  prminf  12941  topnfn  13191  prdsvallem  13219  prdsval  13220  fnmgp  13799  rhmex  14034  rmodislmodlem  14227  rmodislmod  14228  cnfldstr  14435  zring0  14477  fnpsr  14544  mplvalcoe  14567  fnmpl  14570  xmetunirn  14945  tgioo  15141  tgqioo  15142  addcncntoplem  15148  expcncf  15196  dveflem  15313  dvef  15314  efcn  15355  sinhalfpilem  15378  sincosq1lem  15412  sincosq4sgn  15416  cosq23lt0  15420  coseq00topi  15422  coseq0negpitopi  15423  tangtx  15425  sincos4thpi  15427  sincos6thpi  15429  pigt3  15431  cos02pilt1  15438  cos0pilt1  15439  2logb9irr  15558  2logb3irr  15560  2logb9irrALT  15561  sqrt2cxp2logb9e3  15562  2irrexpq  15563  2logb9irrap  15564  2irrexpqap  15565  1sgm2ppw  15582  lgseisenlem1  15662  lgseisenlem2  15663  lgsquadlem1  15669  ex-fl  15861  ex-exp  15863  trilpolemeq1  16181