Theorem mp3an 1332

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

Syntax hints:   -> wi 4   /\ w3a 973

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

This theorem depends on definitions:  df-bi 116  df-3an 975

This theorem is referenced by:  vtocl3  2786  raltp  3640  rextp  3641  ordtriexmidlem  4503  ordtri2or2exmidlem  4510  onsucelsucexmidlem  4513  ordsoexmid  4546  funopg  5232  ftp  5681  caovass  6013  caovdi  6032  mptexw  6092  ofmres  6115  mpofvexi  6185  mpoexw  6192  dmtpos  6235  rntpos  6236  dftpos3  6241  tpostpos  6243  mapsnen  6789  xpcomen  6805  mapxpen  6826  xpmapenlem  6827  unfiexmid  6895  1lt2pi  7302  1lt2nq  7368  halfnqq  7372  m1p1sr  7722  m1m1sr  7723  suplocsrlempr  7769  addassi  7928  mulassi  7929  adddii  7930  adddiri  7931  lttri  8024  lelttri  8025  ltletri  8026  letri  8027  mul12i  8065  mul32i  8066  add12i  8082  add32i  8083  addcani  8101  addcan2i  8102  subaddi  8206  subadd2i  8207  subsub23i  8209  addsubassi  8210  addsubi  8211  subcani  8212  subcan2i  8213  pnncani  8214  subdii  8326  subdiri  8327  ltadd2i  8339  ltadd1i  8421  leadd1i  8422  leadd2i  8423  ltsubaddi  8424  lesubaddi  8425  ltsubadd2i  8426  lesubadd2i  8427  ltaddsubi  8428  gtapii  8553  mulcanapi  8585  divclapi  8671  divcanap2i  8672  divcanap1i  8673  divrecapi  8674  divcanap3i  8675  divcanap4i  8676  divassapi  8685  divdirapi  8686  div23api  8687  div11api  8688  sup3exmid  8873  1mhlfehlf  9096  halfpm6th  9098  3halfnz  9309  unirnioo  9930  nnenom  10390  inftonninf  10397  m1expcl2  10498  i4  10578  expnass  10581  bcn1  10692  hashinfom  10712  abs3difi  11120  0.999...  11484  ef01bndlem  11719  cos1bnd  11722  cos2bnd  11723  sin4lt0  11729  3dvdsdec  11824  3dvds2dec  11825  ndvdsi  11892  flodddiv4  11893  3lcm2e6woprm  12040  6lcm4e12  12041  3prm  12082  znnen  12353  ennnfonelem1  12362  prminf  12410  topnfn  12584  xmetunirn  13152  tgioo  13340  tgqioo  13341  addcncntoplem  13345  expcncf  13386  dveflem  13481  dvef  13482  efcn  13483  sinhalfpilem  13506  sincosq1lem  13540  sincosq4sgn  13544  cosq23lt0  13548  coseq00topi  13550  coseq0negpitopi  13551  tangtx  13553  sincos4thpi  13555  sincos6thpi  13557  pigt3  13559  cos02pilt1  13566  cos0pilt1  13567  2logb9irr  13683  2logb3irr  13685  2logb9irrALT  13686  sqrt2cxp2logb9e3  13687  2irrexpq  13688  2logb9irrap  13689  2irrexpqap  13690  ex-fl  13760  ex-exp  13762  trilpolemeq1  14072