Theorem mp3an 1371

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

Syntax hints:   -> wi 4   /\ w3a 1002

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 1004

This theorem is referenced by:  vtocl3  2857  raltp  3723  rextp  3724  ordtriexmidlem  4611  ordtri2or2exmidlem  4618  onsucelsucexmidlem  4621  ordsoexmid  4654  funopg  5352  ftp  5828  caovass  6172  caovdi  6191  mptexw  6264  ofmres  6287  mpofvexi  6358  mpoexw  6365  dmtpos  6408  rntpos  6409  dftpos3  6414  tpostpos  6416  mapsnen  6972  xpcomen  6994  mapxpen  7017  xpmapenlem  7018  unfiexmid  7091  1lt2pi  7538  1lt2nq  7604  halfnqq  7608  m1p1sr  7958  m1m1sr  7959  suplocsrlempr  8005  addassi  8165  mulassi  8166  adddii  8167  adddiri  8168  lttri  8262  lelttri  8263  ltletri  8264  letri  8265  mul12i  8303  mul32i  8304  add12i  8320  add32i  8321  addcani  8339  addcan2i  8340  subaddi  8444  subadd2i  8445  subsub23i  8447  addsubassi  8448  addsubi  8449  subcani  8450  subcan2i  8451  pnncani  8452  subdii  8564  subdiri  8565  ltadd2i  8578  ltadd1i  8660  leadd1i  8661  leadd2i  8662  ltsubaddi  8663  lesubaddi  8664  ltsubadd2i  8665  lesubadd2i  8666  ltaddsubi  8667  gtapii  8792  mulcanapi  8825  divclapi  8912  divcanap2i  8913  divcanap1i  8914  divrecapi  8915  divcanap3i  8916  divcanap4i  8917  divassapi  8926  divdirapi  8927  div23api  8928  div11api  8929  sup3exmid  9115  1mhlfehlf  9340  halfpm6th  9342  3halfnz  9555  addex  9859  mulex  9860  unirnioo  10181  nnenom  10668  inftonninf  10676  m1expcl2  10795  i4  10876  expnass  10879  bcn1  10992  hashinfom  11012  abs3difi  11683  0.999...  12048  ef01bndlem  12283  cos1bnd  12286  cos2bnd  12287  sin4lt0  12294  3dvdsdec  12392  3dvds2dec  12393  ndvdsi  12460  flodddiv4  12463  3lcm2e6woprm  12624  6lcm4e12  12625  3prm  12666  dec2dvds  12950  modxai  12955  gcdi  12959  numexp2x  12964  2exp5  12971  2exp11  12975  znnen  12985  ennnfonelem1  12994  prminf  13042  topnfn  13293  prdsvallem  13321  prdsval  13322  fnmgp  13901  rhmex  14137  rmodislmodlem  14330  rmodislmod  14331  cnfldstr  14538  zring0  14580  fnpsr  14647  mplvalcoe  14670  fnmpl  14673  xmetunirn  15048  tgioo  15244  tgqioo  15245  addcncntoplem  15251  expcncf  15299  dveflem  15416  dvef  15417  efcn  15458  sinhalfpilem  15481  sincosq1lem  15515  sincosq4sgn  15519  cosq23lt0  15523  coseq00topi  15525  coseq0negpitopi  15526  tangtx  15528  sincos4thpi  15530  sincos6thpi  15532  pigt3  15534  cos02pilt1  15541  cos0pilt1  15542  2logb9irr  15661  2logb3irr  15663  2logb9irrALT  15664  sqrt2cxp2logb9e3  15665  2irrexpq  15666  2logb9irrap  15667  2irrexpqap  15668  1sgm2ppw  15685  lgseisenlem1  15765  lgseisenlem2  15766  lgsquadlem1  15772  upgr2wlkdc  16121  ex-fl  16172  ex-exp  16174  trilpolemeq1  16496