Theorem mp3an 1374

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

Syntax hints:   -> wi 4   /\ w3a 1005

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 1007

This theorem is referenced by:  vtocl3  2873  raltp  3748  rextp  3749  ordtriexmidlem  4643  ordtri2or2exmidlem  4650  onsucelsucexmidlem  4653  ordsoexmid  4686  funopg  5388  ftp  5871  caovass  6217  caovdi  6236  mptexw  6308  ofmres  6331  mpofvexi  6404  mpoexw  6411  dmtpos  6489  rntpos  6490  dftpos3  6495  tpostpos  6497  mapsnen  7055  xpcomen  7080  mapxpen  7103  xpmapenlem  7104  unfiexmid  7180  1lt2pi  7657  1lt2nq  7723  halfnqq  7727  m1p1sr  8077  m1m1sr  8078  suplocsrlempr  8124  addassi  8284  mulassi  8285  adddii  8286  adddiri  8287  lttri  8380  lelttri  8381  ltletri  8382  letri  8383  mul12i  8421  mul32i  8422  add12i  8438  add32i  8439  addcani  8457  addcan2i  8458  subaddi  8562  subadd2i  8563  subsub23i  8565  addsubassi  8566  addsubi  8567  subcani  8568  subcan2i  8569  pnncani  8570  subdii  8682  subdiri  8683  ltadd2i  8696  ltadd1i  8778  leadd1i  8779  leadd2i  8780  ltsubaddi  8781  lesubaddi  8782  ltsubadd2i  8783  lesubadd2i  8784  ltaddsubi  8785  gtapii  8910  mulcanapi  8943  divclapi  9030  divcanap2i  9031  divcanap1i  9032  divrecapi  9033  divcanap3i  9034  divcanap4i  9035  divassapi  9044  divdirapi  9045  div23api  9046  div11api  9047  sup3exmid  9233  1mhlfehlf  9458  halfpm6th  9460  3halfnz  9678  addex  9987  mulex  9988  unirnioo  10309  nnenom  10800  inftonninf  10808  m1expcl2  10927  i4  11008  expnass  11011  bcn1  11124  hashinfom  11145  abs3difi  11845  0.999...  12211  ef01bndlem  12446  cos1bnd  12449  cos2bnd  12450  sin4lt0  12457  3dvdsdec  12555  3dvds2dec  12556  ndvdsi  12623  flodddiv4  12626  3lcm2e6woprm  12787  6lcm4e12  12788  3prm  12829  dec2dvds  13113  modxai  13118  gcdi  13122  numexp2x  13127  2exp5  13134  2exp11  13138  ballotfilem2  13149  ballotfilem4  13159  znnen  13166  ennnfonelem1  13175  prminf  13223  topnfn  13474  prdsvallem  13502  prdsval  13503  fnmgp  14083  rhmex  14319  rmodislmodlem  14515  rmodislmod  14516  cnfldstr  14723  zring0  14765  fnpsr  14832  mplvalcoe  14862  fnmpl  14865  xmetunirn  15240  tgioo  15436  tgqioo  15437  addcncntoplem  15443  expcncf  15491  dveflem  15608  dvef  15609  efcn  15650  sinhalfpilem  15673  sincosq1lem  15707  sincosq4sgn  15711  cosq23lt0  15715  coseq00topi  15717  coseq0negpitopi  15718  tangtx  15720  sincos4thpi  15722  sincos6thpi  15724  pigt3  15726  cos02pilt1  15733  cos0pilt1  15734  2logb9irr  15853  2logb3irr  15855  2logb9irrALT  15856  sqrt2cxp2logb9e3  15857  2irrexpq  15858  2logb9irrap  15859  2irrexpqap  15860  1sgm2ppw  15880  lgseisenlem1  15960  lgseisenlem2  15961  lgsquadlem1  15967  upgr2wlkdc  16389  konigsberglem1  16500  konigsberglem2  16501  konigsberglem3  16502  konigsberglem5  16504  ex-fl  16510  ex-exp  16512  repiecelem  16826  repiecege0  16828  trilpolemeq1  16841