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  8431  lelttri  8432  ltletri  8433  letri  8434  mul12i  8473  mul32i  8474  add12i  8490  add32i  8491  addcani  8509  addcan2i  8510  subaddi  8614  subadd2i  8615  subsub23i  8617  addsubassi  8618  addsubi  8619  subcani  8620  subcan2i  8621  pnncani  8622  subdii  8735  subdiri  8736  ltadd2i  8749  ltadd1i  8831  leadd1i  8832  leadd2i  8833  ltsubaddi  8834  lesubaddi  8835  ltsubadd2i  8836  lesubadd2i  8837  ltaddsubi  8838  gtapii  8964  mulcanapi  8997  divclapi  9086  divcanap2i  9087  divcanap1i  9088  divrecapi  9089  divcanap3i  9090  divcanap4i  9091  divassapi  9100  divdirapi  9101  div23api  9102  div11api  9103  sup3exmid  9289  1mhlfehlf  9527  halfpm6th  9529  3halfnz  9747  addex  10062  mulex  10063  unirnioo  10385  nnenom  10884  inftonninf  10892  m1expcl2  11011  i4  11092  expnass  11095  bcn1  11210  hashinfom  11231  abs3difi  11937  0.999...  12304  ef01bndlem  12539  cos1bnd  12542  cos2bnd  12543  sin4lt0  12550  3dvdsdec  12648  3dvds2dec  12649  ndvdsi  12716  flodddiv4  12719  3lcm2e6woprm  12880  6lcm4e12  12881  3prm  12922  dec2dvds  13210  modxai  13215  gcdi  13220  numexp2x  13225  2exp5  13232  2exp11  13236  ballotfilem2  13277  ballotfilemafi  13287  ballotfilembfi  13288  ballotfilem4  13290  ballotfilemi1  13294  ballotfilemth  13330  znnen  13338  ennnfonelem1  13347  prminf  13395  topnfn  13647  prdsvallem  13670  prdsval  14222  fnmgp  14268  rhmex  14513  rmodislmodlem  14736  rmodislmod  14737  cnfldstr  14944  zring0  14984  fnpsr  15100  mplvalcoe  15130  fnmpl  15133  xmetunirn  15508  tgioo  15704  tgqioo  15705  addcncntoplem  15711  expcncf  15759  dveflem  15876  dvef  15877  efcn  15918  sinhalfpilem  15942  sincosq1lem  15976  sincosq4sgn  15980  cosq23lt0  15984  coseq00topi  15986  coseq0negpitopi  15987  tangtx  15989  sincos4thpi  15991  sincos6thpi  15993  pigt3  15995  cos02pilt1  16002  cos0pilt1  16003  2logb9irr  16126  2logb3irr  16128  2logb9irrALT  16129  sqrt2cxp2logb9e3  16130  2irrexpq  16131  2logb9irrap  16132  2irrexpqap  16133  log2tlbndlog2  16139  log2ublem1  16140  log2ublem2  16141  log2ublog2  16143  1sgm2ppw  16190  ppiqub  16194  bclbnd  16205  lgseisenlem1  16287  lgseisenlem2  16288  lgsquadlem1  16294  upgr2wlkdc  16716  konigsberglem1  16827  konigsberglem2  16828  konigsberglem3  16829  konigsberglem5  16831  ex-fl  16837  ex-exp  16839  repiecelem  17172  repiecege0  17174  trilpolemeq1  17187