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  4668  ordtri2or2exmidlem  4675  onsucelsucexmidlem  4678  ordsoexmid  4711  funopg  5414  ftp  5903  caovass  6253  caovdi  6272  mptexw  6346  ofmres  6373  mpofvexi  6446  mpoexw  6453  dmtpos  6532  rntpos  6533  dftpos3  6538  tpostpos  6540  mapsnen  7106  xpcomen  7131  mapxpen  7154  xpmapenlem  7155  unfiexmid  7231  1lt2pi  7713  1lt2nq  7779  halfnqq  7783  m1p1sr  8133  m1m1sr  8134  suplocsrlempr  8180  addassi  8340  mulassi  8341  adddii  8342  adddiri  8343  lttri  8437  lelttri  8438  ltletri  8439  letri  8440  mul12i  8479  mul32i  8480  add12i  8496  add32i  8497  addcani  8515  addcan2i  8516  subaddi  8620  subadd2i  8621  subsub23i  8623  addsubassi  8624  addsubi  8625  subcani  8626  subcan2i  8627  pnncani  8628  subdii  8741  subdiri  8742  ltadd2i  8755  ltadd1i  8837  leadd1i  8838  leadd2i  8839  ltsubaddi  8840  lesubaddi  8841  ltsubadd2i  8842  lesubadd2i  8843  ltaddsubi  8844  gtapii  8970  mulcanapi  9003  divclapi  9092  divcanap2i  9093  divcanap1i  9094  divrecapi  9095  divcanap3i  9096  divcanap4i  9097  divassapi  9106  divdirapi  9107  div23api  9108  div11api  9109  sup3exmid  9295  1mhlfehlf  9534  halfpm6th  9536  3halfnz  9753  addex  10068  mulex  10069  unirnioo  10391  nnenom  10891  inftonninf  10899  m1expcl2  11018  i4  11099  expnass  11102  bcn1  11217  hashinfom  11238  abs3difi  11944  0.999...  12312  ef01bndlem  12547  cos1bnd  12550  cos2bnd  12551  sin4lt0  12558  3dvdsdec  12656  3dvds2dec  12657  ndvdsi  12724  flodddiv4  12727  3lcm2e6woprm  12888  6lcm4e12  12889  3prm  12930  dec2dvds  13218  modxai  13223  gcdi  13228  numexp2x  13233  2exp5  13240  2exp11  13244  ballotfilem2  13285  ballotfilemafi  13295  ballotfilembfi  13296  ballotfilem4  13298  ballotfilemi1  13302  ballotfilemth  13338  znnen  13346  ennnfonelem1  13355  prminf  13403  topnfn  13656  prdsvallem  13679  prdsval  14279  fnmgp  14325  rhmex  14572  rmodislmodlem  14795  rmodislmod  14796  cnfldstr  15003  zring0  15043  fnpsr  15161  mplvalg  15222  fnmpl  15225  xmetunirn  15601  tgioo  15797  tgqioo  15798  addcncntoplem  15804  expcncf  15852  dveflem  15969  dvef  15970  efcn  16011  sinhalfpilem  16035  sincosq1lem  16069  sincosq4sgn  16073  cosq23lt0  16077  coseq00topi  16079  coseq0negpitopi  16080  tangtx  16082  sincos4thpi  16084  sincos6thpi  16086  pigt3  16088  cos02pilt1  16096  cos0pilt1  16097  2logb9irr  16224  2logb3irr  16226  2logb9irrALT  16227  sqrt2cxp2logb9e3  16228  2irrexpq  16229  2logb9irrap  16230  2irrexpqap  16231  log2tlbndlog2  16237  log2ublem1  16238  log2ublem2  16239  log2ublog2  16241  1sgm2ppw  16306  ppiqub  16310  bclbnd  16324  bposlem8  16335  lgseisenlem1  16411  lgseisenlem2  16412  lgsquadlem1  16418  upgr2wlkdc  16840  konigsberglem1  16951  konigsberglem2  16952  konigsberglem3  16953  konigsberglem5  16955  ex-fl  16961  ex-exp  16963  repiecelem  17297  repiecege0  17299  trilpolemeq1  17313