Theorem mp3an 1319

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

Syntax hints:   -> wi 4   /\ w3a 963

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 965

This theorem is referenced by:  vtocl3  2768  raltp  3616  rextp  3617  ordtriexmidlem  4477  ordtri2or2exmidlem  4484  onsucelsucexmidlem  4487  ordsoexmid  4520  funopg  5203  ftp  5651  caovass  5978  caovdi  5997  ofmres  6081  mpofvexi  6151  dmtpos  6200  rntpos  6201  dftpos3  6206  tpostpos  6208  mapsnen  6753  xpcomen  6769  mapxpen  6790  xpmapenlem  6791  unfiexmid  6859  1lt2pi  7254  1lt2nq  7320  halfnqq  7324  m1p1sr  7674  m1m1sr  7675  suplocsrlempr  7721  addassi  7880  mulassi  7881  adddii  7882  adddiri  7883  lttri  7975  lelttri  7976  ltletri  7977  letri  7978  mul12i  8015  mul32i  8016  add12i  8032  add32i  8033  addcani  8051  addcan2i  8052  subaddi  8156  subadd2i  8157  subsub23i  8159  addsubassi  8160  addsubi  8161  subcani  8162  subcan2i  8163  pnncani  8164  subdii  8276  subdiri  8277  ltadd2i  8289  ltadd1i  8371  leadd1i  8372  leadd2i  8373  ltsubaddi  8374  lesubaddi  8375  ltsubadd2i  8376  lesubadd2i  8377  ltaddsubi  8378  gtapii  8503  mulcanapi  8535  divclapi  8621  divcanap2i  8622  divcanap1i  8623  divrecapi  8624  divcanap3i  8625  divcanap4i  8626  divassapi  8635  divdirapi  8636  div23api  8637  div11api  8638  sup3exmid  8822  1mhlfehlf  9045  halfpm6th  9047  3halfnz  9255  unirnioo  9870  nnenom  10326  inftonninf  10333  m1expcl2  10434  i4  10514  expnass  10517  bcn1  10625  hashinfom  10645  abs3difi  11049  0.999...  11411  ef01bndlem  11646  cos1bnd  11649  cos2bnd  11650  sin4lt0  11656  3dvdsdec  11748  3dvds2dec  11749  ndvdsi  11816  flodddiv4  11817  3lcm2e6woprm  11954  6lcm4e12  11955  3prm  11996  znnen  12110  ennnfonelem1  12119  topnfn  12327  xmetunirn  12729  tgioo  12917  tgqioo  12918  addcncntoplem  12922  expcncf  12963  dveflem  13058  dvef  13059  efcn  13060  sinhalfpilem  13083  sincosq1lem  13117  sincosq4sgn  13121  cosq23lt0  13125  coseq00topi  13127  coseq0negpitopi  13128  tangtx  13130  sincos4thpi  13132  sincos6thpi  13134  pigt3  13136  cos02pilt1  13143  cos0pilt1  13144  2logb9irr  13259  2logb3irr  13261  2logb9irrALT  13262  sqrt2cxp2logb9e3  13263  2irrexpq  13264  2logb9irrap  13265  2irrexpqap  13266  ex-fl  13272  ex-exp  13274  trilpolemeq1  13582