Theorem mp3an 1337

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

Syntax hints:   -> wi 4   /\ w3a 978

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 980

This theorem is referenced by:  vtocl3  2793  raltp  3649  rextp  3650  ordtriexmidlem  4517  ordtri2or2exmidlem  4524  onsucelsucexmidlem  4527  ordsoexmid  4560  funopg  5249  ftp  5700  caovass  6032  caovdi  6051  mptexw  6111  ofmres  6134  mpofvexi  6204  mpoexw  6211  dmtpos  6254  rntpos  6255  dftpos3  6260  tpostpos  6262  mapsnen  6808  xpcomen  6824  mapxpen  6845  xpmapenlem  6846  unfiexmid  6914  1lt2pi  7336  1lt2nq  7402  halfnqq  7406  m1p1sr  7756  m1m1sr  7757  suplocsrlempr  7803  addassi  7962  mulassi  7963  adddii  7964  adddiri  7965  lttri  8058  lelttri  8059  ltletri  8060  letri  8061  mul12i  8099  mul32i  8100  add12i  8116  add32i  8117  addcani  8135  addcan2i  8136  subaddi  8240  subadd2i  8241  subsub23i  8243  addsubassi  8244  addsubi  8245  subcani  8246  subcan2i  8247  pnncani  8248  subdii  8360  subdiri  8361  ltadd2i  8373  ltadd1i  8455  leadd1i  8456  leadd2i  8457  ltsubaddi  8458  lesubaddi  8459  ltsubadd2i  8460  lesubadd2i  8461  ltaddsubi  8462  gtapii  8587  mulcanapi  8620  divclapi  8707  divcanap2i  8708  divcanap1i  8709  divrecapi  8710  divcanap3i  8711  divcanap4i  8712  divassapi  8721  divdirapi  8722  div23api  8723  div11api  8724  sup3exmid  8910  1mhlfehlf  9133  halfpm6th  9135  3halfnz  9346  addex  9647  mulex  9648  unirnioo  9969  nnenom  10429  inftonninf  10436  m1expcl2  10537  i4  10617  expnass  10620  bcn1  10731  hashinfom  10751  abs3difi  11158  0.999...  11522  ef01bndlem  11757  cos1bnd  11760  cos2bnd  11761  sin4lt0  11767  3dvdsdec  11862  3dvds2dec  11863  ndvdsi  11930  flodddiv4  11931  3lcm2e6woprm  12078  6lcm4e12  12079  3prm  12120  znnen  12391  ennnfonelem1  12400  prminf  12448  topnfn  12681  fnmgp  13063  zring0  13359  xmetunirn  13729  tgioo  13917  tgqioo  13918  addcncntoplem  13922  expcncf  13963  dveflem  14058  dvef  14059  efcn  14060  sinhalfpilem  14083  sincosq1lem  14117  sincosq4sgn  14121  cosq23lt0  14125  coseq00topi  14127  coseq0negpitopi  14128  tangtx  14130  sincos4thpi  14132  sincos6thpi  14134  pigt3  14136  cos02pilt1  14143  cos0pilt1  14144  2logb9irr  14260  2logb3irr  14262  2logb9irrALT  14263  sqrt2cxp2logb9e3  14264  2irrexpq  14265  2logb9irrap  14266  2irrexpqap  14267  ex-fl  14337  ex-exp  14339  trilpolemeq1  14648