Theorem mp3an 1378

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

This proof depends on syntax axioms:   -> wi 4   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  vtocl3  2879  raltp  3766  rextp  3767  ordtriexmidlem  4666  ordtri2or2exmidlem  4673  onsucelsucexmidlem  4676  ordsoexmid  4709  funopg  5411  ftp  5900  caovass  6250  caovdi  6269  mptexw  6342  ofmres  6369  mpofvexi  6442  mpoexw  6449  dmtpos  6527  rntpos  6528  dftpos3  6533  tpostpos  6535  mapsnen  7100  xpcomen  7125  mapxpen  7148  xpmapenlem  7149  unfiexmid  7225  1lt2pi  7707  1lt2nq  7773  halfnqq  7777  m1p1sr  8127  m1m1sr  8128  suplocsrlempr  8174  addassi  8334  mulassi  8335  adddii  8336  adddiri  8337  lttri  8430  lelttri  8431  ltletri  8432  letri  8433  mul12i  8472  mul32i  8473  add12i  8489  add32i  8490  addcani  8508  addcan2i  8509  subaddi  8613  subadd2i  8614  subsub23i  8616  addsubassi  8617  addsubi  8618  subcani  8619  subcan2i  8620  pnncani  8621  subdii  8734  subdiri  8735  ltadd2i  8748  ltadd1i  8830  leadd1i  8831  leadd2i  8832  ltsubaddi  8833  lesubaddi  8834  ltsubadd2i  8835  lesubadd2i  8836  ltaddsubi  8837  gtapii  8962  mulcanapi  8995  divclapi  9084  divcanap2i  9085  divcanap1i  9086  divrecapi  9087  divcanap3i  9088  divcanap4i  9089  divassapi  9098  divdirapi  9099  div23api  9100  div11api  9101  sup3exmid  9287  1mhlfehlf  9523  halfpm6th  9525  3halfnz  9743  addex  10052  mulex  10053  unirnioo  10375  nnenom  10871  inftonninf  10879  m1expcl2  10998  i4  11079  expnass  11082  bcn1  11196  hashinfom  11217  abs3difi  11922  0.999...  12288  ef01bndlem  12523  cos1bnd  12526  cos2bnd  12527  sin4lt0  12534  3dvdsdec  12632  3dvds2dec  12633  ndvdsi  12700  flodddiv4  12703  3lcm2e6woprm  12864  6lcm4e12  12865  3prm  12906  dec2dvds  13190  modxai  13195  gcdi  13199  numexp2x  13204  2exp5  13211  2exp11  13215  ballotfilem2  13228  ballotfilemafi  13238  ballotfilembfi  13239  ballotfilem4  13241  ballotfilemi1  13245  ballotfilemth  13281  znnen  13289  ennnfonelem1  13298  prminf  13346  topnfn  13598  prdsvallem  13621  prdsval  14173  fnmgp  14219  rhmex  14464  rmodislmodlem  14687  rmodislmod  14688  cnfldstr  14895  zring0  14935  fnpsr  15051  mplvalcoe  15081  fnmpl  15084  xmetunirn  15459  tgioo  15655  tgqioo  15656  addcncntoplem  15662  expcncf  15710  dveflem  15827  dvef  15828  efcn  15869  sinhalfpilem  15892  sincosq1lem  15926  sincosq4sgn  15930  cosq23lt0  15934  coseq00topi  15936  coseq0negpitopi  15937  tangtx  15939  sincos4thpi  15941  sincos6thpi  15943  pigt3  15945  cos02pilt1  15952  cos0pilt1  15953  2logb9irr  16073  2logb3irr  16075  2logb9irrALT  16076  sqrt2cxp2logb9e3  16077  2irrexpq  16078  2logb9irrap  16079  2irrexpqap  16080  log2tlbndlog2  16082  log2ublem1  16083  log2ublem2  16084  log2ublog2  16086  1sgm2ppw  16109  lgseisenlem1  16189  lgseisenlem2  16190  lgsquadlem1  16196  upgr2wlkdc  16618  konigsberglem1  16729  konigsberglem2  16730  konigsberglem3  16731  konigsberglem5  16733  ex-fl  16739  ex-exp  16741  repiecelem  17074  repiecege0  17076  trilpolemeq1  17089