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  2820  raltp  3679  rextp  3680  ordtriexmidlem  4555  ordtri2or2exmidlem  4562  onsucelsucexmidlem  4565  ordsoexmid  4598  funopg  5292  ftp  5747  caovass  6084  caovdi  6103  mptexw  6170  ofmres  6193  mpofvexi  6264  mpoexw  6271  dmtpos  6314  rntpos  6315  dftpos3  6320  tpostpos  6322  mapsnen  6870  xpcomen  6886  mapxpen  6909  xpmapenlem  6910  unfiexmid  6979  1lt2pi  7407  1lt2nq  7473  halfnqq  7477  m1p1sr  7827  m1m1sr  7828  suplocsrlempr  7874  addassi  8034  mulassi  8035  adddii  8036  adddiri  8037  lttri  8131  lelttri  8132  ltletri  8133  letri  8134  mul12i  8172  mul32i  8173  add12i  8189  add32i  8190  addcani  8208  addcan2i  8209  subaddi  8313  subadd2i  8314  subsub23i  8316  addsubassi  8317  addsubi  8318  subcani  8319  subcan2i  8320  pnncani  8321  subdii  8433  subdiri  8434  ltadd2i  8447  ltadd1i  8529  leadd1i  8530  leadd2i  8531  ltsubaddi  8532  lesubaddi  8533  ltsubadd2i  8534  lesubadd2i  8535  ltaddsubi  8536  gtapii  8661  mulcanapi  8694  divclapi  8781  divcanap2i  8782  divcanap1i  8783  divrecapi  8784  divcanap3i  8785  divcanap4i  8786  divassapi  8795  divdirapi  8796  div23api  8797  div11api  8798  sup3exmid  8984  1mhlfehlf  9209  halfpm6th  9211  3halfnz  9423  addex  9726  mulex  9727  unirnioo  10048  nnenom  10526  inftonninf  10534  m1expcl2  10653  i4  10734  expnass  10737  bcn1  10850  hashinfom  10870  abs3difi  11321  0.999...  11686  ef01bndlem  11921  cos1bnd  11924  cos2bnd  11925  sin4lt0  11932  3dvdsdec  12030  3dvds2dec  12031  ndvdsi  12098  flodddiv4  12101  3lcm2e6woprm  12254  6lcm4e12  12255  3prm  12296  dec2dvds  12580  modxai  12585  gcdi  12589  numexp2x  12594  2exp5  12601  2exp11  12605  znnen  12615  ennnfonelem1  12624  prminf  12672  topnfn  12915  fnmgp  13478  rhmex  13713  rmodislmodlem  13906  rmodislmod  13907  cnfldstr  14114  zring0  14156  fnpsr  14221  xmetunirn  14594  tgioo  14790  tgqioo  14791  addcncntoplem  14797  expcncf  14845  dveflem  14962  dvef  14963  efcn  15004  sinhalfpilem  15027  sincosq1lem  15061  sincosq4sgn  15065  cosq23lt0  15069  coseq00topi  15071  coseq0negpitopi  15072  tangtx  15074  sincos4thpi  15076  sincos6thpi  15078  pigt3  15080  cos02pilt1  15087  cos0pilt1  15088  2logb9irr  15207  2logb3irr  15209  2logb9irrALT  15210  sqrt2cxp2logb9e3  15211  2irrexpq  15212  2logb9irrap  15213  2irrexpqap  15214  1sgm2ppw  15231  lgseisenlem1  15311  lgseisenlem2  15312  lgsquadlem1  15318  ex-fl  15371  ex-exp  15373  trilpolemeq1  15684