Theorem mp3an 1348

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

Syntax hints:   -> wi 4   /\ w3a 980

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 982

This theorem is referenced by:  vtocl3  2817  raltp  3676  rextp  3677  ordtriexmidlem  4552  ordtri2or2exmidlem  4559  onsucelsucexmidlem  4562  ordsoexmid  4595  funopg  5289  ftp  5744  caovass  6081  caovdi  6100  mptexw  6167  ofmres  6190  mpofvexi  6261  mpoexw  6268  dmtpos  6311  rntpos  6312  dftpos3  6317  tpostpos  6319  mapsnen  6867  xpcomen  6883  mapxpen  6906  xpmapenlem  6907  unfiexmid  6976  1lt2pi  7402  1lt2nq  7468  halfnqq  7472  m1p1sr  7822  m1m1sr  7823  suplocsrlempr  7869  addassi  8029  mulassi  8030  adddii  8031  adddiri  8032  lttri  8126  lelttri  8127  ltletri  8128  letri  8129  mul12i  8167  mul32i  8168  add12i  8184  add32i  8185  addcani  8203  addcan2i  8204  subaddi  8308  subadd2i  8309  subsub23i  8311  addsubassi  8312  addsubi  8313  subcani  8314  subcan2i  8315  pnncani  8316  subdii  8428  subdiri  8429  ltadd2i  8441  ltadd1i  8523  leadd1i  8524  leadd2i  8525  ltsubaddi  8526  lesubaddi  8527  ltsubadd2i  8528  lesubadd2i  8529  ltaddsubi  8530  gtapii  8655  mulcanapi  8688  divclapi  8775  divcanap2i  8776  divcanap1i  8777  divrecapi  8778  divcanap3i  8779  divcanap4i  8780  divassapi  8789  divdirapi  8790  div23api  8791  div11api  8792  sup3exmid  8978  1mhlfehlf  9203  halfpm6th  9205  3halfnz  9417  addex  9720  mulex  9721  unirnioo  10042  nnenom  10508  inftonninf  10516  m1expcl2  10635  i4  10716  expnass  10719  bcn1  10832  hashinfom  10852  abs3difi  11303  0.999...  11667  ef01bndlem  11902  cos1bnd  11905  cos2bnd  11906  sin4lt0  11913  3dvdsdec  12009  3dvds2dec  12010  ndvdsi  12077  flodddiv4  12078  3lcm2e6woprm  12227  6lcm4e12  12228  3prm  12269  znnen  12558  ennnfonelem1  12567  prminf  12615  topnfn  12858  fnmgp  13421  rhmex  13656  rmodislmodlem  13849  rmodislmod  13850  cnfldstr  14057  zring0  14099  fnpsr  14164  xmetunirn  14537  tgioo  14733  tgqioo  14734  addcncntoplem  14740  expcncf  14788  dveflem  14905  dvef  14906  efcn  14944  sinhalfpilem  14967  sincosq1lem  15001  sincosq4sgn  15005  cosq23lt0  15009  coseq00topi  15011  coseq0negpitopi  15012  tangtx  15014  sincos4thpi  15016  sincos6thpi  15018  pigt3  15020  cos02pilt1  15027  cos0pilt1  15028  2logb9irr  15144  2logb3irr  15146  2logb9irrALT  15147  sqrt2cxp2logb9e3  15148  2irrexpq  15149  2logb9irrap  15150  2irrexpqap  15151  lgseisenlem1  15227  lgseisenlem2  15228  lgsquadlem1  15234  ex-fl  15287  ex-exp  15289  trilpolemeq1  15600